# Subtyping variance of dependent product types

**URL:** <https://discourse.rocq-prover.org/t/subtyping-variance-of-dependent-product-types/2457>\
**Category:** Using Rocq\
**Created:** [October 29, 2024, 10:05am UTC](https://discourse.rocq-prover.org/t/subtyping-variance-of-dependent-product-types/2457 "2024-10-29T10:05:06Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [October 29, 2024, 10:05am UTC](https://discourse.rocq-prover.org/t/subtyping-variance-of-dependent-product-types/2457/1 "2024-10-29T10:05:06Z")

</div>

The manual gives this subtyping rule for product types [here](https://coq.inria.fr/doc/V8.19.0/refman/language/cic.html):

> If E[Γ] ⊢ T =\_{βδιζη} U and E[Γ :: (x : T)] ⊢ T' ≤\_{βδιζη} U' then E[Γ] ⊢ ∀ x : T, T' ≤\_{βδιζη} ∀ x : U, U'.

What surprises me here is the T =\_{βδιζη} U where I would have expected T ≥\_{βδιζη} U. I think that in programming languages with static typing and subtyping, the function type A → B is usually contravariant in A, but this definition says that in Coq it is invariant.

I tested this code:

```auto
Parameter X : Set.
Check X : Type.

Parameter Y : nat -> Set.
Check Y : nat -> Type.

Parameter Z : Type -> nat.
Check Z : Set -> nat.

```

The result is very surprising to me: the first to `Check` commands pass, as expected, and the third _also_ passes, but instead of

```auto
Z : Set -> nat

```

Coq says

```auto
(fun x : Set => Z x) : Set -> nat

```

so it seems like `Z` was automatically η-expanded to yield the right type.

What’s going on behind the scenes here? What’s the reason product types are invariant in the “index” type? How does Coq decide when to η-expand a term to convert it to a certain type? Where can I read more about this?

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [October 29, 2024, 10:11am UTC](https://discourse.rocq-prover.org/t/subtyping-variance-of-dependent-product-types/2457/2 "2024-10-29T10:11:15Z")

</div>

> What’s the reason product types are invariant in the “index” type?

We generally call it the domain not the index.  
It makes model construction easier, for instance in the set model.

> How does Coq decide when to η-expand a term to convert it to a certain type?

The coercion system when trying to coerce `f : A-> B` to `A' -> B'` tries to produce `fun x : A' => coe_B_to_B' (f (coe_A'_to_A x))`.  
in your example the sub coercions are the identity thanks to cumulativity

* * *

see also [Activating contravariant subtyping of dependent function types by herbelin · Pull Request #13270 · coq/coq · GitHub](https://github.com/coq/coq/pull/13270)

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [October 30, 2024, 12:50am UTC](https://discourse.rocq-prover.org/t/subtyping-variance-of-dependent-product-types/2457/3 "2024-10-30T00:50:38Z")

</div>

From [https://inria.hal.science/hal-04077552v2/document](https://inria.hal.science/hal-04077552v2/document)

> 1This restriction comes from the fact that it is difficult to model contravariant cumulativity in set-theoretic models [Timany and Sozeau 2018](https://inria.hal.science/hal-01952037). Whether cumulativity could be contravariant on the left-hand side of an arrow or not is still the subject of ongoing theoretical investigations.