**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In dependent type theory, and particularly homotopy type theory, an **identification** is a word sometimes used for an inhabitant of an identity type.

Thus an identification $p:a=b$ provides a “reason”, a “witness”, or a “proof” that $a$ and $b$ “are equal”, or more precisely a *way in which to identify them*. The distinguishing feature of homotopy type theory is that in general, there may be more than one way to identify two things, i.e. more than one identification between two given elements.

Last revised on May 21, 2022 at 13:06:28. See the history of this page for a list of all contributions to it.