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

):

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?