Technical reports
Categorical combinators for the calculus of constructions
Eike Ritter
October 1990, 43 pages
DOI: 10.48456/tr-208
Abstract
This report describes the derivation of a small and intuitive set of categorical combinators for the Calculus of Constructions. The choice of an appropriate categorical semantics is the crucial step. A modification of Ehrhard’s higher-order closed summable fibrations, yielding so called CC-categories, turns out to be the appropriate underlying categorical structure. Standard techniques can then be used to derive the combinators. The combinators can be turned directly into the classifying category for the Calculus of Constructions. This establishes a precise connection between the calculus, the combinators and the CC-categories.
Full text
PDF (2.8 MB)
BibTeX record
@TechReport{UCAM-CL-TR-208, author = {Ritter, Eike}, title = {{Categorical combinators for the calculus of constructions}}, year = 1990, month = oct, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-208.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-208}, number = {UCAM-CL-TR-208} }