[[!redirects identity]] [[!redirects identity types]] [[!redirects identities]] [[!redirects path]] [[!redirects paths]] [[!redirects equality]] [[!redirects equal]] ## Idea ## The identity type has elements that are witnesses to the "sameness" of elements. ## Definition ## The identity type $=_A : A \to A \to \mathcal{U}$ can be defined as the [[inductive type]] with the following constructor: * for any $a:A$, an element $refl_A: a=_A a$ ## See also ## [[higher inductive type]] ## References ## [[HoTT book]] category: type theory