Related Work, Extensions and Directions of Further Investigations
In the previous chapters we have studied the Calculus of Constructions following a classical pattern. We have introduced a class of structures called doctrines of constructions in Chapter 1 and studied several instances of this notion in Chapter 2 (realizability and retract models). In Chapter 3 we have defined an axiomatization of the calculus and the interpretation of this calculus in arbitrary doctrines of constructions and then have proved a correctness theorem. Finally in Chapter 4 we have shown the existence of a term model. Further we have shown that only provably correct types and objects get an interpretation in the term model and only those equality judgments which can be derived in the calculus are valid under interpretation in the term model.
KeywordsIdentity Type Dependent Type Unique Section Chapter Versus Unique Morphism
Unable to display preview. Download preview PDF.