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