nLab explicit conversion

Idea

In type theory, there are many ways to represent the notion of conversion of terms from one to another in the syntax. Usually, this is represented by untyped or typed judgmental equality as a judgment $a \equiv b$ or $a \equiv b:A$ respectively. Explicit conversion is the representation of conversion as terms of a type $p:a \equiv b$.

In objective type theory and other weak type theories which don’t have a judgmental equality as a judgment, explicit conversion is used for definitions and for beta-conversion and eta-conversion, and is represented by identifications $p:a =_A b$ for elements and by equivalences $e:A \simeq B$ for types.

 Related concepts

• judgmental equality

 References

• Floris van Doorn, Herman Geuvers, and Freek Wiedijk, Explicit convertibility proofs in pure type systems. Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, ACM. 2013, pp. 25–36 (pdf)

• Theo Winterhalter, Formalisation and Meta-Theory of Type Theory (github)