Correctness of the Interpretation of the Calculus of Constructions in Doctrines of Constructions
According to Gerard Huet and Thierry Coquand the Calculus of Constructions is a typed λ-calculus where type expressions themselves can contain λ-expressions as subterms. The original presentation in [Col] is characterized by a lot of overloading which has puzzled many readers as there products of types, functional abstraction and universal quantification were represented by one and the same syntactic construct, namely [x:A]B. Another instance of overloading was their systematic mixing of two aspects of propositions, namely propositions as objects of type Prop and propositions as types. This ambiguity we avoid by the type-forming construct Proof, which when applied to an object p of type Prop gives the type Proof(p) of proofs of the proposition p.
KeywordsInduction Hypothesis Type Expression Interpretation Function Equal Section Type Prop
Unable to display preview. Download preview PDF.