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.
Follow this link