[[!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 ## * [[dependent type theory]] * [[homotopy type]] * [[identity system]] * [[homotopy type theory]] * [[higher inductive type]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: type theory