**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. Alternatives to the term identification include **identity**, **path**, or **equality**, though those phrases are also used in different contexts.

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 January 19, 2023 at 16:10:47. See the history of this page for a list of all contributions to it.