Categorical semantics of functional type theory with explicit substitutions, formalized in Agda.
This project depends on agda-categories library.
- The semantics is given by the correspondence between λ×-theories and Cartesian Closed Categories (CCC).
- We use de Bruijn indices, as opposed to named variables, because we don't want to bother with α-equivalent terms.
- We use explicit substitutions because shift/substitution are tedious to deal with, and more importantly, explicit substitutions scale to dependent type theories.
- We don't consider untyped terms, only typed terms.
- Soundness
- Completeness
- Roy L. Crole. Categories for Types. Cambridge University Press. 1993.
- Jonathan Sterling. Algebraic Type Theory and the Gluing Construction. CMU HoTT Seminar. 2019.