Rafaël Bocquet: For the metatheory of type theory, internal sconing is enough

Abstract: When doing the metatheory of dependent type theory, one proves properties of the syntax of type theory, such as canonicity (which characterizes the closed terms of the syntax), and normalization (which determines the normal forms of open terms). In general, proving properties of closed terms is easier than proving properties of open terms. Categorically, these proofs involve gluing constructions. In the case of closed terms, a simpler instance of gluing is used, known as sconing.

In this talk, I will explain how to use sconing even when proving properties of open terms. This involves seeing the open terms of the syntactic model as the closed terms of an internal model.

This is joint work with Ambrus Kaposi and Christian Sattler.