We investigate the relationship between the monotonic (→) and the antimonotonic exponentiation (➾) in a type system with subtyping. We present a model in which we can develop both exponentiations at the same time. In this model the monotonic and the antimonotonic exponentiation enjoy a duality, namely α➾β=∁(α→∁β) where ∁ is the type constructor complement. We give a sound and complete system of axioms for the type system with the type constructors →, ➾, ∪, ∩, ∁, ⊥, T.