Some types in the calculus of constructions
Consider the following types, and verify that they are well formed in
the Calculus of Constructions. For each of these types, give a
natural informally defined inhabitant.
(nat->nat)->Prop
(nat->nat)->(nat->nat)->Prop
nat->nat->Set
Solution
Follow this link
Going home
Pierre Castéran