[[!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 ## ### In Martin-Loef type theory ### 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$ ### In cubical type theory ### ### In higher observational type theory ### Identity types have the following formation rule $$\frac{A:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A) \quad b:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_A(a, b):\mathcal{U}}$$ ## See also ## * [[dependent type theory]] * [[dependent identity type]] * [[homotopy type]] * [[identity system]] * [[homotopy type theory]] * [[higher inductive type]] * [[transport]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Mike Shulman, Towards a Third-Generation HOTT Part 1 ([slides](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-04-28.pdf), [video](https://www.youtube.com/watch?v=FrxkVzItMzA)) category: type theory