Eliminating reflection from type theory
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau · 2019
Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they make it possible to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL and more recently in Andromeda.