Why is η-reduction illegal?

Miscellaneous
1

Hi,

I am trying to wrap my head around calculus of inductive constructions, but I stuck at η-reduction, I don’t understand why it is illegal. Here is my train of thought:

If there is a term (as I interpret it: a function that can be applied to a term of type Type(2) and produces a term of type Type(1)):

f : ∀ x : Type ( 2 ) , Type ( 1 )

then there is no way to construct the term:

λ x : Type ( 1 ) , ( f   x ) : ∀ x : Type ( 1 ) , Type ( 1 )

because this lambda abstraction’s argument is of type Type(1) and f expects the parameter of type Type(2).

Could anyone show flaws in my reasoning?

2

Anything of Type(1) can be typed as Type(2), please see an example below.

Universes i j k.
Constraint i < j.
Constraint j < k.
Variable T : Type@{j}.
Fail Check T : Type@{i}.
Check T : Type@{k}.
3

The problem is the other way around: an eta-redex Type(1) -> Type(1) could reduce to an f : Type(2) -> Type(1) which is not a subtype of Type(1) -> Type(1) because we don’t have contravariance in the cumulativity/conversion relation. So it is not a type preserving reduction