Department of Computer Science and Technology

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}
}