Definitional Functoriality for Dependent (Sub)Types -- Extended version

Théo Laurent, Meven Lennon-Bertrand, Kenji Maillard

Dependently typed proof assistant rely crucially on definitional equality, which relates types and terms that are automatically identified in the underlying type theory. This paper…