Invariant Type Constructor

type-theory

Definition

Invariant Type Constructor

Let $A$ and $B$ be type. A type constructor $K$ is called invariant if it is neither covariant nor contravariant:

$$A\le B⟹\left(K[A]\cancel{\le }K[B]\wedge K[B]\cancel{\le }K[A]\right)$$

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