The manual gives this subtyping rule for product types here:

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:

```
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

```
Z : Set -> nat
```

Coq says

```
(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?