nLab explicit conversion



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 aba \equiv b or ab:Aa \equiv b:A respectively. Explicit conversion is the representation of conversion as terms of a type p:abp: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= Abp:a =_A b for elements and by equivalences e:ABe:A \simeq B for types.


Created on October 2, 2023 at 15:46:59. See the history of this page for a list of all contributions to it.