Equality, Quasi-Implicit Products, and Large Eliminations

Vilhelm Sjöberg, Aaron Stump

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including impli…