<p>The contravariant rule for functions would indeed work, and it is supported by the semantics in <a href="https://drops.dagstuhl.de/opus/volltexte/2022/15748/pdf/LIPIcs-CSL-2022-28.pdf" rel="noreferrer">Generalized Universe Hierarchies and First-Class
Universe Levels</a>.</p>
<p>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 <a href="https://arxiv.org/pdf/1710.03912.pdf" rel="noreferrer">Consistency of the Predicative Calculus of
Cumulative Inductive Constructions (pCuIC)</a>.</p>

CC BY-SA 4.0
2022-10-18T06:19:48.967Z
2022-10-18T06:19:48.967Z
András Kovács
<p>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.</p>
<p>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.</p>
<p><strong>Definition 2.3 (cumulativity relation)</strong> The cumulativity relation <span class="math-container">$\preceq$</span> is defined to be smalled binary relation over terms such that</p>
<ol>
<li><span class="math-container">$\preceq$</span> is a partial order with respect to conversion.</li>
<li><span class="math-container">$Prop$</span> <span class="math-container">$\preceq$</span> <span class="math-container">$Type_0$</span> <span class="math-container">$\preceq$</span> <span class="math-container">$Type_1$</span> <span class="math-container">$\preceq$</span> ...</li>
<li>if <span class="math-container">$A_1 \simeq B_1$</span> and <span class="math-container">$A_2 \preceq B_2$</span>, then <span class="math-container">$\Pi(x : A_1).A_2 \preceq \Pi(x : B_1).B_2$</span>.</li>
</ol>
<p>I want to ask, why is <span class="math-container">$\preceq$</span> only used in the codomain of <span class="math-container">$\Pi$</span>-types in case 3? Factoring in contravariance for function subtyping, why wouldn't the following work?</p>
<ol start="3">
<li>if <span class="math-container">$B_1 \preceq A_1$</span> and <span class="math-container">$A_2 \preceq B_2$</span> then <span class="math-container">$\Pi(x : A_1).A_2 \preceq \Pi(x : B_1).B_2$</span>.</li>
</ol>

<type-theory><dependent-type>
Dependent type theory and definitions of cumulativity
Qiancheng Fu
# Dependent type theory and definitions of cumulativity

(Asked by: username_0 on 2022-10-18)

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

**Tags:** type-theory, dependent-type

---

## 1 answers

### Answer by username_1 on 2022-10-18. Score: 6 | Accepted answer

The contravariant rule for functions would indeed work, and it is supported by the semantics in [Generalized Universe Hierarchies and First-Class
Universe Levels](https://drops.dagstuhl.de/opus/volltexte/2022/15748/pdf/LIPIcs-CSL-2022-28.pdf).

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)](https://arxiv.org/pdf/1710.03912.pdf).


---

