equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
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 type theory – where one understands every piece of data (every “term”) as being of a given type which specifies its operational behaviour – identity types (maybe better: identification types) $Id_X$ are the types of those terms which serve as “witnesses” or “certificates” (see at “propositions as types”) of identification of terms of type $X$.
What exactly this means depends on the nature of the ambient type theory and the choices for the inference rules of the identity types (see at extensional and intensional type theory). In some setups (see below), having a term of identity type means much the same as having an equality in classical mathematics, and for this (historical) reason identity types are often denoted simply by equality signs, for better or worse.
But the power of the notion of identity types goes beyond this classical situation and results from the fact that they may give the notion of equality a constructive meaning (“propositional equality”). Taking this constructive principle of identity types to its logical conclusion, leads – notably in Martin-Löf dependent type theory, see below – to identity types which themselves have identity types, reflecting identifications-of-identification, and so on, paralleling the higher structure of homotopies and homotopies of homotopies in homotopy theory, whence one refers to type theories with such identity types also as homotopy type theories.
The inference rules for identity types in Martin-Löf-/homotopy type theory (ML identity types) may be understood as follows:
(0) – There is a notion of identification. To start with, for every type $X$ and any pair $x_1, x_2 : X$ of its terms, let’s denote the type of identifications of $x_1$ with $x_2$ by $Id_X(x_1,x_2)$ (other common notation for identity types is “$x_1 =_{{}_X} x_2$” which, when adopted, requires authors to make up new symbols, like $\equiv$, for actual equalities). In the jargon of dependent type theory this means that there is a type formation rule for identity types as shown on the left here:
Beware that in type theory generally and specifically in this entry further below, the self-identification certificate $id_X$ is often denoted “$refl$”, alluding to reflexivity of an equality relation.
On the right we are indicating, here and in the following, the categorical semantics of the judgement on the left, under the relation between type theory and category theory, specifically between dependent type theory and LCC category theory. The lay reader may take the diagrams shown on the right as intuitive illustrations of dependent types as bundles of types, their terms as sections, etc. Technically, these are diagrams in some locally cartesian closed (model) category. (Beware that we are showing an actual interval object $I$ for ease of illustration, but its existence is not required by the rules for ML identity types: $X^I$ may denote an object that does not arise as an internal hom. Making the interval object syntactically explicit leads to “cubical identity types”, see below.)
The archetypical example is the (classical model structure on) SimplicialSets (with interval object $I = \Delta[1]$ the 1-simplex) in which case all fibrations shown are Kan fibrations between Kan complexes which may be thought of as models for (fibrations of) $\infty$-groupoids. But the power of ML identity types is that they may just as well be interpreted in much more general model categories, such as the injective model structure on simplicial presheaves over any simplicial site, modelling $\infty$-toposes of $\infty$-stacks.
Now to consider three “self-evident” properties of the notion of identifications (Latin quotes from Gottfried Leibniz $\sim$ 1700, p. 228 and p. 230 in Gerhard 1890), expressed in type theoretic language:
(I) – All data is identified with itself.
This “first law of thought” is the term introduction-rule for identity types:
(IIa) – Substitution of identifications preserves computations. This is Leibniz’s “salva veritate”-principle phrased operationally/constructively:
In homotopy type theory this has come to be known as transport, compatible with the fact that its categorical semantics is that of path lifting in Kan fibrations, which in the case of discrete fibrations (covering spaces) underlying flat principal bundles or flat vector bundles (“local systems”) is the parallel transport/holonomy/monodromy of the corresponding flat connection.
(IIb) – An identification identifies itself with a self-identification. While one may argue that this is still “self-evident”, it is more subtle than the previous two principles. In particular, it concerns an identification of identifications, a possibility that was ignored by the logical forefathers (Leibniz highlights at least the composition of identifications, such as $p \cdot id_x$).
In type theory language, the existence of these identifications-of-identifications is the following judgement (with $\underset{x' : X}{\coprod}$ denoting the dependent sum-type):
(An intuitive categorical semantics is schematically indicated on the right, with the certificate $p_*$ pictured as a copy of $p$ on the bottom together with a “path-of-paths” relating the concatenated path $p \bullet id_x$ to $p$. This is valid when realized in the model structure on simplicial sets or any model structure on simplicial presheaves, literally given by triangular diagrams as above, these being 1-simplices in $X^I \underset{ev_0}{\times} \{x\}$ when hom-adjointly regarded as 2-simplices in $X$. However, this is not literally what the principle says when expressed in type theory, where there is no concatenated path $p \bullet id_x$ — although after we have identity types with all of their rules, it can be proved equivalent.)
(J) $\Leftrightarrow$ (II) – Id-induction. Applying the above transport rule (IIa) to the identifications-of-identifications provided by the composition rule (IIb) yields the following “J-rule”, which was not known to the forefathers:
(This “induction-rule” for identity types was proposed in Martin-Löf 1975, §1.7 and p. 94; its modern rendering as a formal inference rule is due to Nordström, Petersson & Smith 1990, §8.1. It may be understood as the term elimination rule (see below) or the induction-principle (see further below) for identity types, whence also called “Id-elimination” or “Id-induction”, or similar.)
While the J-rule is naturally understood as the application of the transport rule (IIa) to the identifications-of-identification provided by the composition rule (IIb), it also implies both these rules, hence is equivalent to their combination (IIa and IIb). (This fact was briefly mentioned by Coquand 2011, slides 26+28 and amplified by Ladyman & Presnell 2015; the detailed proof is spelled out by Götz 2018, §4.2.)
Importantly, as indicated on the right above, the categorical semantics of the J-rule is manifestly that of the left lifting property of $X \xrightarrow{diag} X^I$ against all fibrations, which means that this rule manifestly prescribes the interpretation of identity types by “very good path space objects ” in the sense of model category theory (cf. Shulman 2012 III, Slide 34; Riehl 2022, §1.1). It is this fact which connects ML identity types to the notion of homotopy in homotopy theory, hence to the interpretation of Martin-Löf dependent type theory as “homotopy type theory” with categorical semantics in locally cartesian closed $\infty$-categories.
Incidentally, another immediate consequence of the J-rule is the following refinement of the transport rule (IIa), which is closer to what Leibniz may have recognized:
(IIa’) – Substitution of identifications preserves identifications.
Besides the Martin-Löf identity types above there are other version of identity types considered in the literature, notably there are variants which share the homotopy-theoretic interpretation but differ in some technical details:
For instance, cubical identity types (such as Swan identity types) are the identity types in cubical type theory, which are such that that applied to the type universe they provably (computationally) satisfy the univalence axiom.
Namely, the J-rule in Martin-Löf dependent type theory above still involves an ordinary definitional equality in its statement that the lifted term $\widehat{\sigma}$ is equal to the given term $\sigma$ after restriction to self-identitfication. Cubical identity types essentially turns this equality itself into a propositional equality.
Similarly, higher observational type theory has its appropriate version of higher identity types.
Notice that higher identity types restricted specifically to h-sets behave again more like ordinary equality does (by definition of h-set).
More specifically, there are also strict identity types, strictly without an homotopy-theoretic interpretation:
Since there are two notions of equality in type theory, there are similarly two notions of the J-rule in type theory. The definitional J-rule states that $J(x, x, \mathrm{refl}(x))$ is definitionally equal to $c(x)$ (i.e. $J(x, x, \mathrm{refl}(x)) = c(x)$). This is in contrast to the propositional J-rule or typal J-rule above, which states that there is a dependent term
Identity types which satisfy the definitional J-rule could be called strict identity types, while identity types which only satisfy the propositional J-rule could be called weak identity types, in parallel with similar definitions for a (weak and strict) Tarski universe. Martin-Löf identity types come in both strict and weak flavours. However, most other identity types in the literature, such as cubical path types and higher observational identity types, are only weak identity types.
The definition of identity types was originally given in explicit form by Martin-Löf, in terms of introduction and elimination rules. Later, it was realized that this was a special case of the general notion of inductive type. We will discuss both formulations.
The rules for forming identity types and terms are as follows (expressed in sequent calculus). First the rule that defines the identity type itself, as a dependent type, in some context $\Gamma$.
Now the basic “introduction” rule, which says that everything is equal to itself in a canonical way.
To a category theorist, it might be more natural to call this $1_X$. The traditional notation $r(x)$ indicates that this is a canonical proof of the reflexivity of equality.
Then we have the “elimination” rule, which is easily the most subtle and powerful.
Ignore the presence of the additional context $\Delta$ for now; it is unnecessary if we also have dependent product types. The elimination rule then says that if:
then we can construct a canonically defined term $J(t;x,y,p):C(x,y,p)$ for any $x$, $y$, and $p:Id_A(x,y)$, by “transporting” the term $t$ along the proof of equality $p$. In homotopical or categorical models, this can be viewed as a “path-lifting” property, i.e. that the display maps are some sort of fibration. This can be made precise with the identity type weak factorization system?.
A particular case is when $C$ is a term representing a proposition according to the propositions-as-types philosophy. In this case, the elimination rule says that in order to prove a statement is true about all $x,y,p$, it suffices to prove it in the special case for $x,x,r(x)$.
Finally, we have the “computation” or β-reduction? rule. This says that if we substitute along a reflexivity proof, nothing happens. There are two possible computation rules, which result in strict and weak identity types respectively
computation rule for strict identity types
Note that the equality $=$ in the conclusion of this computation rule is definitional equality, not an instance of the identity/equality type itself.
computation rule for weak identity types
These rules may seem a little ad-hoc, but they are actually a particular case of the general notion of inductive type.
Using inductive types the notion of identity types is encoded in a single line (see Licata 11, Shulman 12).
In Coq notation we can say
Inductive id {A} : A -> A -> Type := idpath : forall x, id x x.
In other words, the identity type of $A$ is inductively generated by reflexivity $x = x$ (the “first law of thought”), in the same way that the natural numbers are inductively generated by zero and successor. From this, the above introduction, elimination, and computation rules are all derived automatically.
This is the approach to Martin-Lof identity types taken by implementations of homotopy type theory in proof assistants such as Coq or Agda. See, for instance, Overture.v
An essentially equivalent way to give the definition, due to Paulin-Mohring, is
Inductive id {A} (x:A) : A -> Type := idpath : id x x.
The difference here is that now $x$ is a parameter of the inductive definition rather than an index. In other words, the first definition says “for each type $A$, we have a type $Id_A$ dependent on $A\times A$, inductively defined by a constructor $idpath$ which takes an element $x\colon A$ as input and yields output in $Id_A(x,x)$” while the second definition says “for each type $A$ and each element $x\colon A$, we have a type $Id_A(x)$ dependent on $A$, inductively defined by a constructor $idpath$ which takes no input and yields output in $Id_A(x)(x)$.” The two formulations can be proven equivalent, but sometimes one is more convenient than the other.
Almost all types in type theory can be given both β-reduction? and η-reduction rules. $\beta$-reduction specifies what happens when we apply an eliminator to a term obtained by a constructor; $\eta$-reduction specifies the reverse. Above we have formulated only the $\beta$-reduction rule for identity types; the $\eta$-conversion rule would be the following:
This says that if $C$ is a type which we can use the eliminator $J$ to construct a term of, but we already have a term $t$ of that type, then if we restrict $t$ to reflexivity inputs and then apply $J$ to construct a term of type $C$, the result is the same as the term $t$ we started with. As in the $\beta$-reduction rule, the $=$ in the conclusion refers to definitional equality.
This $\eta$-conversion rule has some very strong consequences. For instance, suppose $x\colon A$, $y\colon A$, and $p\colon Id_A(x,y)$, and let $C \coloneqq A$. Then with $t=x$, the $\eta$-conversion rule tells us that $x = J(x[x/y,r(x)/p];x,y,p)$. And with $t=y$, the $\eta$-conversion rule tells us that $y = J(y[x/y,r(x)/p];x,y,p)$. But substituting $x$ for $y$ (and $r(x)$ for $p$) in the term $y$ simply yields the term $x$, which is the same as the result of substituting $x$ for $y$ and $r(x)$ for $p$ in the term $x$. Thus, we have
In other words, if $Id_A(x,y)$ is inhabited (that is, $x$ and $y$ are propositionally equal) then in fact $x$ and $y$ are definitionally equal. Moreover, by a similar argument we can show that
(Here we are eliminating into the type $C(x,y,p) \coloneqq Id_A(x,y)$. The term $r(x)$ may be regarded as belonging to this type, because we have already shown that $x$ and $y$ are definitionally equal.)
Thus, the definitional $\eta$-conversion rule for identity types implies that the type theory is extensional in a very strong sense. (This was observed already in (Streicher).) For this reason, in homotopy type theory we do not assume the $\eta$-conversion rule for identity types.
This sort of extensionality in type theory is also problematic for non-homotopical reasons: since type-checking in dependent type theory depends on definitional equality, but the above rule implies that definitional equality depends on inhabitation of identity types, this makes definitional equality and hence type-checking undecidable in the formal computational sense. Thus, $\eta$-conversion for identity types is often omitted (as in Coq).
On the other hand, it is possible to prove a propositional version of $\eta$-conversion using only the identity types as defined above without definitional $\eta$-conversion. In other words, given the hypotheses of the above $\eta$-conversion rule, we can construct a term belonging to the type
This has none of the bad consequences of definitional $\eta$-conversion, and in particular does not imply that the type theory is extensional. The argument that $p\colon Id_A(x,y)$ implies $x=y$ becomes the tautologous statement that if $p\colon Id_A(x,y)$ then $p\colon Id_A(x,y)$, while the subsequent argument that $p= r(x)$ fails because $x$ and $y$ are no longer definitionally equal, so $r(x)$ does not have type $Id_A(x,y)$. We can transport it along $p$ to obtain a term of this type, but then we obtain only that $p$ is equal to the transport of $r(x)$ along $p$, which is a perfectly intensional/homotopical statement.
Identity types in observational type theory and higher observational type theory are defined in a different manner than they are in Martin-Löf type theory.
In higher observational type theory, identity types have the same formation rule as Martin-Löf identity types do:
However, it does not have global elimination or computation rules. Instead, it has a local computation rule for each particular type. For example, the identity type of the product type $A \times B$ has the following computation rule:
We are working in a dependent type theory with Tarski-style universes.
The identity types in a universe in higher observational type theory have the following formation rule:
We define a general congruence term called ap
and the reflexivity terms:
and computation rules for identity functions
and for constant functions $y$
Thus, ap is a higher dimensional explicit substitution. There are definitional equalities
for constant term $t$.
Let $A \cong_\mathcal{U} B$ be the type of bijective correspondences between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$, and let $\mathrm{id}_\mathcal{U}(A, B)$ be the identity type between two terms of a universe $A:\mathcal{U}$ and $B:\mathcal{U}$. Then there are rules
Given a term of a universe $A:\mathcal{U}$
with terms representing singleton contractibility?.
The primary identity types are the nondependent cubical path types in cubical type theory. Like the identity types in higher observational type theory, they do not satisfy the definitional version of identification elimination; only the propositional version of identification elimination. See cubical path type for more information on the construction of the cubical path types.
Some cubical type theories include a second identity type which satisfies the definitional version of identification elimination. This is called Swan's identity type?, and is defined by the following rules:
Identity types in cubical type theory are called path types and are defined using a primitive interval.
We discuss the categorical semantics for identity types in the extensional case, and identity types in the categorical semantics of homotopy type theory in the intensional case.
In categorical models of extensional type theory, generally every morphism of the category is allowed to represent a dependent type, and the extensional identity types are represented by diagonal maps $A\to A\times A$.
By contrast, in models of intensional type theory, there is only a particular class of display maps or fibrations which are allowed to represent dependent types, and intensional identity types are represented by path objects $P A \to A \times A$.
Both of these cases apply in particular to models in the category of contexts of the type theory itself, i.e. the term model.
By the standard construction of mapping path spaces out of path space objects, the existence of identity types allows one to construct a weak factorization system.
Conversely, since any weak factorization system gives rise to path objects by factorization of diagonal maps, one may hope to construct a model of type theory with identity types in a category equipped with a WFS $(L,R)$. There are four obstacles in the way of such a construction.
In order to handle the additional context $\Delta$ in the explicit definition above, it turns out to be necessary to assume that $L$-maps are preserved by pullback along $R$-maps between $R$-objects. (Such a condition is also necessary in order to interpret type-theoretic dependent products in a locally cartesian closed category.)
This enables us to define identity types with their elimination and computation rules “locally”, i.e. for each type individually. However, every construction in type theory is stable under substitution. This means that if $y\colon Y\vdash A(y)\colon Type$ is a dependent type and $f\colon X\to Y$ is a morphism, then the identity type $x\colon X \vdash Id_{A(f(x))}(-,-)\colon Type$ is the same whether we first construct $Id_{A(y)}$ and then substitute $f(x)$ for $y$, or first substitute $f(x)$ for $y$ to obtain $A(f(x))$ and then construct its identity type. In order for this to hold up to isomorphism, we need to require that the WFS have stable path objects — a choice of path object data in each slice category which is preserved by pullback. In Warren 2008 it is shown that any simplicial model category in which the cofibrations are the monomorphisms can be equipped with stable path objects, while Garner & van den Berg 2011 it is shown that the presence of internal path-categories also suffices.
The eliminator term $J$ of identity types in type theory is also preserved by substitution. This imposes an additional coherence requirement which is tricky to obtain categorically. See Warren 2008 and Garner & van den Berg 2011 for methods that ensure this, such as by invoking an algebraic weak factorization system. It can also be handled a la Voevodsky by using a (possibly univalent) universe.
Finally, substitution in type theory is strictly functorial/associative, whereas it is modeled categorically by pullback which is generally not strictly so. This is a general issue with the categorical interpretation of dependent type theory, not something specific to identity types. It can be resolved by passing to a split fibration which is equivalent to the codomain fibration, or by making use of a universe. See categorical model of dependent types.
Assume then that a category $\mathcal{C}$ with suitable WFSs has been chosen, for instance a type-theoretic model category. Then
The interpretation of a type $\vdash A : Type$ is as a fibrant object $[\vdash A : Type]$ which we will just write “$A$” for short.
type formation
The identity type $a, b : A \vdash Id_A(a,b) : Type$ is interpreted as the path space object fibration
term introduction
By definition of path space object, there exists a lift $\sigma$ in
By the universal property of the pullback this is equivalently a section of the pullback of the path space object along the diagonal morphism $(id,id) : A \to A \times A$.
Since $(id, id)^* A^I$ is the interpretation of the substitution
$a : A \vdash Id_A (a,a) : Type$ in this sense $\sigma$ is now the interpretation of a term $a : A \vdash r_A : Id_A (a,a)$.
term elimination
A type depending on an identity type
is interpreted as a fibration
The substitution $C(a,a,r_a)$ is interpreted by the pullback
Therefore a term $t : C(a,a,r_a)$ is interpreted as a section of this pullback
By the universal property of the pullback, this is equivalently a morphism $t$ in
The elimination rule says that given such $t$, there exists a compatible section of $C \to A^I$. If we redraw the previous diagram as a square, then this section is a lift in that diagram
In particular, if $C$ itself is the pullback of a fibration $D \to B$ along a morphism $A^I \to B$, then $r$ has the left lifting property also against that fibration
So the term elimination rule says that the interpretaton $A \to A^I$ of $a : A \vdash r(a) : Id_A (a,a)$ has the left lifting property against all fibrations, hence that $A \to A^I$ is to be interpreted as an acyclic cofibration.
Some of the first work noticing the homotopical / higher-categorical interpretation of identity types (see below) focused on the fact that the tower of iterated identity types of a type has the structure of an internal algebraic ∞-groupoid.
In retrospect, this is roughly an algebraic version of the standard fact that every object of a model category (or more generally a category of fibrant objects or a category with a weak factorization system) admits a simplicial resolution which is an internal Kan complex, i.e. a nonalgebraic $\infty$-groupoid. Note, however, that the first technical condition above (stability of $L$-maps under pullback along $R$-maps) seems to be necessary for the algebraic version of the result to go through.
The above Latin excerpts by Gottfried Leibniz are taken from
whose English translation is given in:
The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in
and in the modern form of inference rules in
with early survey in §1.0.1 of:
See also (?):
Per Martin-Löf, p. 169 (17 of 23) in: Constructive Mathematics and Computer Programming, Studies in Logic and the Foundations of Mathematics Volume 104, 1982, Pages 153-175 (doi:10.1016/S0049-237X(09)70189-2)
Per Martin-Löf, p. 31-34 in: Intuitionistic type theory, Lecture notes Padua 1984 (notes by Giovanni Sambin), Bibliopolis, Napoli (1984) (pdf, pdf)
The observation that the Id-induction principle (the J-rule) is equivalent to transport (“salva veritate”) together with contractibility of the type of identifications (“composition with self-identifications”) is stated in:
further highlighted in
and the proof of the equivalence is spelled out in:
Discussion of issues of extensional/intensional type theory:
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh, (1995) (ECS-LFCS-95-327, pdf)
Thomas Streicher, Investigations Into Intensional Type Theory, Habilitationsschrift (pdf)
Dan Licata, Understanding Identity Elimination in Homotopy Type Theory, 2011
Mike Shulman, Inductive types and identity types, 2012 (pdf)
https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v
Thorsten Altenkirch and Conor McBride, Towards observational type theory (pdf)
Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)
Mike Shulman, Towards a Third-Generation HOTT Part 2 (slides, video)
Mike Shulman, Towards a Third-Generation HOTT Part 3 (slides, video)
Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) (pdf)
Steve Awodey and Michael Warren, Homotopy theoretic models of identity types, arXiv.
Nicola Gambino, Richard Garner, The identity type weak factorisation system, arXiv
Richard Garner, Benno van den Berg, Topological and simplicial models of identity types, arXiv.
The suggestion that identity types witness groupoid and infinity-groupoid-structure is due to
Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (eds.), Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ISBN:9780198501275, ps pdf)
Steve Awodey, Michael Warren, Homotopy theoretic models of identity type, Mathematical Proceedings of the Cambridge Philosophical Society vol 146, no. 1 (2009) (arXiv:0709.0248)
This is ultimately verified by the observation that the J-rule makes the identity types interpret as very good path space objects in a locally cartesian closed model category (such as the classical model structure on simplicial sets):
reviewed in:
For more see the references at homotopy type theory.
See also
Benno van den Berg, Richard Garner, Types are weak $\omega$-groupoids, Proceedings of the London Mathematical Society 102 2 (2011) 370-394 [arXiv:0812.0298, doi:10.1112/plms/pdq026]
Peter LeFanu Lumsdaine, Weak $\omega$-categories from intensional type theory , (arXiv:0812.0409)
Last revised on September 28, 2022 at 23:51:35. See the history of this page for a list of all contributions to it.