Contravariant Type Constructor

type-theory

Definition

Contravariant Type Constructor

Let $A$ and $B$ be type. A type constructor $K$ is called contravariant if it reverses the subtype relation of the types:

$$A\le B⟹K[B]\le K[A]$$

where $(\cdot \le \cdot )$ denotes the subtype relation.