Dependent type theory and definitions of cumulativity

Question

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

1. $\preceq$ is a partial order with respect to conversion.
2. $Prop$ $\preceq$ $Type_0$ $\preceq$ $Type_1$ $\preceq$ ...
3. 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?

3. 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$.

Answer 1

The contravariant rule for functions would indeed work, and it is supported by the semantics in Generalized Universe Hierarchies and First-Class Universe Levels.

The reason for invariant function domains, as far as I know, is that functions have been modeled in the literature of set-theoretic semantics of cumulativity as (covariant) relations, for example in Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC).