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
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
f expects the parameter of type
Could anyone show flaws in my reasoning?