Many dependent type theories employ an universe hierarchy to compensate for the fact that Type : Type is inconsistent (due to Girard's paradox). A cumulativity relation is then defined to lift terms from lower universes to a higher ones.
The following defintion (snippet) is from Luo's book Computation and Reasoning. The cumulativity relation found in Coq's manual and in Norell's thesis for Agda are all more or less the same as this one.
Definition 2.3 (cumulativity relation) The cumulativity relation $\preceq$ is defined to be smalled binary relation over terms such that
- $\preceq$ is a partial order with respect to conversion.
- $Prop$ $\preceq$ $Type_0$ $\preceq$ $Type_1$ $\preceq$ ...
- if $A_1 \simeq B_1$ and $A_2 \preceq B_2$, then $\Pi(x : A_1).A_2 \preceq \Pi(x : B_1).B_2$.
I want to ask, why is $\preceq$ only used in the codomain of $\Pi$-types in case 3? Factoring in contravariance for function subtyping, why wouldn't the following work?
- if $B_1 \preceq A_1$ and $A_2 \preceq B_2$ then $\Pi(x : A_1).A_2 \preceq \Pi(x : B_1).B_2$.