Covariant Type Constructor

type-theory

Definition

Covariant Type Constructor

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

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

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