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.
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)
Created on October 2, 2023 at 15:46:59. See the history of this page for a list of all contributions to it.