Speaker: Loic Pujet, University of Stockholm, loic@pujet.fr
Tuesday 26 Nov 2024, 14:00, Room 1Z56
Abstract:
Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant.
In this talk, I will present a method based on Pédrot's "prefascist sets" to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to formal proofs of canonicity and normalisation.
This is joint work with Ambrus Kaposi.