[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

nLab identity type

Contents

Context

Equality and Equivalence

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Induction

Contents

Idea

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 XId_X are the types of those terms which serve as “witnesses” or “certificates” (see at “propositions as types”) of identification of terms of type XX.

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.


Note on terminology

There are many different names used for this particular dependent type, as well as many different names used for the terms of this dependent type. These include the following:

name of typename of terms
identity typeidentities
path typepaths
identification typeidentifications
equality typeequalities

These four names have different reasons behind the use of the name:

  • The name “identity type” comes from the fact that the identity type is the canonical one-to-one correspondence a:A,b:AId A(a,b)a:A, b:A \vdash \mathrm{Id}_A(a, b) of the identity equivalence id A:AA\mathrm{id}_A:A \simeq A on a type AA, as well as philosophically that it represents the notion of “identity” of an object; see identity of indiscernibles.

  • The name “path type” comes from either the fact that the identity type is a path space object in the categorical semantics, or that every term in the identity type is represented by a function from the interval type, just as paths in topology are represented by a function from the unit interval.

  • The name “identification type” comes from the fact that elements represents identification certificates in computing, as well as philosophically that it represents the notion of “identifying” two objects together.

  • The name “equality type” comes from the fact that it is the typal equivalent of propositional equality from first order logic with equality.

ML identity types

The inference rules for identity types in Martin-Löf-/homotopy type theory (ML identity types) may be understood as follows (exposition and diagrams follow Myers et al. 2023):


(0) – There is a notion of identification. To start with, for every type XX and any pair x 1,x 2:Xx_1, x_2 : X of its terms, let’s denote the type of identifications of x 1x_1 with x 2x_2 by Id X(x 1,x 2)Id_X(x_1,x_2) (other common notation for identity types is “x 1= Xx 2x_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 Xid_X is often denoted “reflrefl”, 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 II for ease of illustration, but its existence is not required by the rules for ML identity types: X IX^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=Δ[1]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 pid xp \cdot id_x).

In type theory language, the existence of these identifications-of-identifications is the following judgement (with x:X\underset{x' : X}{\coprod} denoting the dependent sum-type):

(An intuitive categorical semantics is schematically indicated on the right, with the certificate p *p_* pictured as a copy of pp on the bottom together with a “path-of-paths” relating the concatenated path pid xp \bullet id_x to pp. 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×ev 0{x}X^I \underset{ev_0}{\times} \{x\} when hom-adjointly regarded as 2-simplices in XX. However, this is not literally what the principle says when expressed in type theory, where there is no concatenated path pid xp \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 XdiagX IX \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.


Cubical identity types

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 judgmental 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 typal 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:

Strict identity types

Since there are two notions of equality in type theory, there are similarly two notions of the J-rule in type theory. The judgmental J-rule states that J(x,x,refl(x))J(x, x, \mathrm{refl}(x)) is judgmentally equal to c(x)c(x) (i.e. J(x,x,refl(x))=c(x)J(x, x, \mathrm{refl}(x)) = c(x)). This is in contrast to the typal J-rule above, which states that there is a dependent term

q(x):Id C(x,x,refl(x))(J(x,x,refl(x)),c(x))q(x):Id_{C(x,x,\mathrm{refl}(x))}(J(x, x, \mathrm{refl}(x)), c(x))

Identity types which satisfy the judgmental J-rule can be called strict identity types, while identity types which only satisfy the typal J-rule can 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.


Definition in Martin-Löf type theory

The definition of identity types was originally given in explicit form by Martin-Löf, in terms of inference rules. Later, it was realized that this was a special case of the general notion of inductive type. We will discuss both formulations.

With inference rules

The inference rules for forming identity types and terms are as follows.

First the rule that defines the identity type itself, as a dependent type, in some context Γ\Gamma.

type formation

ΓA:TypeΓ,x:A,y:AId A(x,y):Type\frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A \vdash Id_A(x,y):Type}

Now the basic “introduction” rule, which says that everything is equal to itself in a canonical way.

term introduction

ΓA:TypeΓ,x:Ar(x):Id A(x,x)\frac{\Gamma \vdash A:Type} {\Gamma, x:A \vdash r(x) : Id_A(x,x)}

To a category theorist, it might be more natural to call this 1 X1_X. The traditional notation r(x)r(x) indicates that this is a canonical proof of the reflexivity of equality.

Then there are the “elimination” rule and the “computation” or beta-reduction rule of identity types, which together result in the induction principle of identity types. There are two different ways to express the elimination and computation rule of identity types, depending on whether one fixes a particular term x:Ax:A for the rules or whether one leaves x:Ax:A as a free variable throughout the rules (Cf UFP13). The latter results in the usual induction principle of identity types, known as path induction (UFP13) or the standard J rule (Kraus and Raumer (2019)), while the former results in based path induction (UFP13) or the Paulin-Mohring J rule (Kraus and Raumer (2019)), since the principle is based at a particular x:Ax:A and was first defined in Paulin-Mohring (1993).

The following rules may seem a little ad-hoc, but they are actually a particular case of the general notion of inductive type.

Standard J rule

Then we have the “elimination” rule, which is easily the most subtle and powerful.

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t(x):C(x,x,r(x))Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)J ̲.t(x,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \quad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t(x):C(x,x,r(x))} {\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J^{\underline{ }.t}(x,y,p) : C(x,y,p)}

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:

  1. for any x,y:Ax,y:A and any reason p:Id A(x,y)p:Id_A(x,y) why they are the same, we have a type C(x,y,p)C(x,y,p)
  2. for any x:Ax:A we have a t(x):C(x,x,r(x))t(x):C(x,x,r(x)),

we can construct a canonically defined term J ̲.t(x,y,p):C(x,y,p)J^{\underline{ }.t}(x,y,p):C(x,y,p) for any xx, yy, and p:Id A(x,y)p:Id_A(x,y), by “transporting” the family of terms t(x)t(x) dependent upon x:Ax:A along the proof of equality pp. 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, which can be made precise with the identity type weak factorization system?.

A particular case is when CC 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,px,y,p, it suffices to prove it in the special case for x,x,r(x)x,x,r(x).

Finally, we have the “computation” or beta-reduction rule. There are two possible computation rules, which result in strict and weak identity types respectively. The computation rule for strict identity types says that if we substitute along a reflexivity proof, nothing happens.

computation rule for strict identity types

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t(x):C(x,x,r(x))Γ,x:A,Δ(x,x,r(x))J ̲.t(x,x,r(x))=t(x)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t(x):C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash J^{\underline{ }.t}(x,x,r(x)) = t(x)}

Note that the equality == in the conclusion of this computation rule is judgmental equality, not an instance of the identity/equality type itself.

The computation rule for weak identity types says that there is a witness that the substitution along a reflexivity proof is equal to the original t(x)t(x).

computation rule for weak identity types

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,Δ(x,x,r(x))t(x):C(x,x,r(x))Γ,x:A,Δ(x,x,r(x))β ̲.t(x):Id C(x,x,r(x))(J ̲.t(x,x,r(x)),t(x))\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, \Delta(x,x,r(x)) \vdash t(x):C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash \beta^{\underline{ }.t}(x):Id_{C(x,x,r(x))}(J^{\underline{ }.t}(x,x,r(x)),t(x))}

If we have dependent product types, we can directly use the dependent function Γt: x:AC(x,x,r(x))\Gamma \vdash t:\prod_{x:A} C(x,x,r(x)) instead of the family of terms t(x)t(x) dependent upon x:Ax:A in the hypothesis. Then the canonically defined term is given by J(t,x,y,p):C(x,y,p)J(t,x,y,p):C(x,y,p) and is dependent upon dependent function t: x:AC(x,x,r(x))t:\prod_{x:A} C(x,x,r(x)) rather than annotated with the family t(x)t(x).

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓt: x:AC(x,x,r(x))Γ,x:A,y:A,p:Id A(x,y)J(t,x,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, y:A, p:Id_A(x,y) \vdash J(t,x,y,p) : C(x,y,p)}
Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓt: x:AC(x,x,r(x))Γ,x:A,Δ(x,x,r(x))J(t,x,x,r(x))=t(x)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash J(t,x,x,r(x)) = t(x)}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by J(λx:A.t(x),x,y,p):C(x,y,p)J(\lambda x:A.t(x),x,y,p):C(x,y,p) and J(λx:A.t(x),x,x,r(x))t(x):C(x,x,r(x))J(\lambda x:A.t(x),x,x,r(x)) \equiv t(x):C(x,x,r(x)). .

Similarly, the canonically defined term in the propositional computation rule is given by the identification β(t,x):Id C(x,x,r(x))(J(t,x,x,r(x)),t(x))\beta(t,x):Id_{C(x,x,r(x))}(J(t,x,x,r(x)),t(x)) and is dependent upon dependent function t: x:AC(x,x,r(x))t:\prod_{x:A} C(x,x,r(x)) rather than annotated with the family t(x)t(x).

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓt: x:AC(x,x,r(x))Γ,x:A,Δ(x,x,r(x))β(t,x):Id C(x,x,r(x))(J(t,x,x,r(x)),t(x))\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(x,x,r(x))} {\Gamma, x:A, \Delta(x,x,r(x)) \vdash \beta(t,x):Id_{C(x,x,r(x))}(J(t,x,x,r(x)),t(x))}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by β(λx:A.t(x),x):Id C(x,x,r(x))(J(λx:A.t(x),x,x,r(x)),t(x))\beta(\lambda x:A.t(x),x):\mathrm{Id}_{C(x,x,r(x))}(J(\lambda x:A.t(x),x,x,r(x)),t(x)). .

Paulin-Mohring J rule

There is another way to express the elimination and computation rules of identity types:

term elimination

Γ,x:A,y:A,p:Id A(x,y)C(x,y,p):TypeΓx:AΓt:C(x,x,r(x))Γ,y:A,p:Id A(x,y)J(x,t,y,p):C(x,y,p)\frac{\Gamma, x:A, y:A, p:Id_A(x,y) \vdash C(x,y,p):Type \quad \Gamma \vdash x:A \quad \Gamma \vdash t:C(x,x,r(x))} {\Gamma, y:A, p:Id_A(x,y) \vdash J(x,t,y,p) : C(x,y,p)}

The elimination rule then says that if:

  1. for any x,y:Ax,y:A and identification p:Id A(x,y)p:Id_A(x,y) why yy is the same as xx, we have a type C(x,y,p)C(x,y,p), and
  2. for any x:Ax:A and t:C(x,x,r(x))t:C(x,x,r(x))

we can construct a canonically defined term J(x,t,y,p):C(x,y,p)J(x,t,y,p):C(x,y,p) for any y:Ay:A, and p:Id A(x,y)p:Id_A(x,y), by “transporting” the term tt along the proof of equality pp. 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, which can be made precise with the identity type weak factorization system?.

According to propositions as types, the elimination rule says that for all xx, in order to prove a statement is true about all y,py,p, it suffices to prove it in the special case for x,r(x)x,r(x).

Finally, we have the “computation” or beta-reduction rule. There are two possible computation rules, which result in strict and weak identity types respectively. The computation rule for strict identity types says that if we substitute along a reflexivity proof, nothing happens.

computation rule for strict identity types

Γ,x:A,y:A,p:Id A(x,y)C(x,y,p):TypeΓx:AΓt:C(x,x,r(x))ΓJ(x,t,x,r(x))=t\frac{\Gamma, x:A, y:A, p:Id_A(x,y) \vdash C(x,y,p):Type \quad \Gamma \vdash x:A \quad \Gamma \vdash t:C(x,x,r(x))} {\Gamma \vdash J(x,t,x,r(x)) = t}

Note that the equality == in the conclusion of this computation rule is judgmental equality, not an instance of the identity/equality type itself.

The computation rule for weak identity types says that there is a witness that the substitution along a reflexivity proof is equal to the original term tt.

computation rule for weak identity types

Γ,x:A,y:A,p:Id A(x,y),Δ(y,p)C(x,y,p):TypeΓx:AΓt:C(x,x,r(x))Γβ(x,t):Id C(x,x,r(x))(J(x,t,x,r(x)),t)\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(y,p) \vdash C(x,y,p):Type \quad \Gamma \vdash x:A \quad \Gamma \vdash t:C(x,x,r(x))} {\Gamma \vdash \beta(x,t):Id_{C(x,x,r(x))}(J(x,t,x,r(x)) ,t)}

Identity types as a negative type

If one has dependent sum types, there is a way of defining the identiy type as a negative type. The idea is that using the inference rules for dependent sum types, the standard J-rule states that the dependent sum type x:A y:Ax= Ay\sum_{x:A} \sum_{y:A} x =_A y is a positive copy of AA with respect to the diagonal function

Δ A(x)(x,(x,refl A(x))): x:A y:Ax= Ay\Delta_{A}(x) \coloneqq (x, (x, \mathrm{refl}_A(x))):\sum_{x:A} \sum_{y:A} x =_A y

However, there is also a negative version of copy types, whose elimination, computation, and uniqueness rules state that the diagonal function is a definitional isomorphism:

  • Elimination rules for negative identity types:
ΓAtypeΓ,z: x:A y:Ax= AyΔ A 1(z):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, z:\sum_{x:A} \sum_{y:A} x =_A y \vdash \Delta_A^{-1}(z):A}
  • Computation rules for negative identity types:
ΓAtypeΓ,x:AΔ A 1(Δ A(x))x:A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \Delta_A^{-1}(\Delta_{A}(x)) \equiv x:A}
  • Uniqueness rules for negative identity types:
ΓAtypeΓ,z: x:A y:Ax= AyΔ A(Δ A 1(z))z: x:A y:Ax= Ay\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, z:\sum_{x:A} \sum_{y:A} x =_A y \vdash \Delta_{A}(\Delta_A^{-1}(z)) \equiv z:\sum_{x:A} \sum_{y:A} x =_A y}

Theorem

The standard J-rule holds: given any type AA, and any type family C(z)C(z) indexed by elements z: x:A y:Ax= Ayz:\sum_{x:A} \sum_{y:A} x =_A y, and given any dependent function t: x:AC(Δ A(x))t:\prod_{x:A} C(\Delta_A(x)) which says that for all elements x:Ax:A, there is an element of the type defined by substituting the diagonal at x:Ax:A into CC, C(Δ A(x))C(\Delta_A(x)), one can construct a dependent function ind x:A y:Ax= Ay(t): z: x:A y:Ax= AyC(z)\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(t):\prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} C(z) such that for all x:Ax:A, ind x:A y:Ax= Ay(Δ A(x))t(x):C(Δ A(x))\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(\Delta_A(x)) \equiv t(x):C(\Delta_A(x)).

Proof

ind x:A y:Ax= Ay(t)\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(t) is defined to be

ind x:A y:Ax= Ay(t)λz: x:A y:Ax= Ay.t(Δ A 1(z))\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(t) \equiv \lambda z:\sum_{x:A} \sum_{y:A} x =_A y.t(\Delta_A^{-1}(z))

and by the computation rules of path types as negative copies, one has that for all x:Ax:A,

Δ A 1(Δ A(x))x\Delta_A^{-1}(\Delta_A(x)) \equiv x

and so by definition of ind x:A y:Ax= Ay(t)\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(t) and the judgmental congruence rules for substitution, one has

ind x:A y:Ax= Ay(t,Δ A(x))t(Δ A 1(Δ A(x)))t(x)\mathrm{ind}_{\sum_{x:A} \sum_{y:A} x =_A y}(t, \Delta_A(x)) \equiv t(\Delta_A^{-1}(\Delta_A(x))) \equiv t(x)

Induction using functions instead of type families

There is a version of the induction principle which uses a type CC and a function f:C x:A y:Ax= Ayf:C \to \sum_{x:A} \sum_{y:A} x =_A y into the type of all identity types in AA, instead of a type family C(x,y,p)C(x, y, p) indexed by x:Ax:A, y:Ay:A, and p:x= Ayp:x =_A y.

Let

Δ Aλx:A.(x,x,refl A(x)):A x:A y:Ax= Ay\Delta_A \coloneqq \lambda x:A.(x, x, \mathrm{refl}_A(x)):A \to \sum_{x:A} \sum_{y:A} x =_A y

be the diagonal function of AA.

The induction principle for the identity type says that given any type CC and function

f:C x:A y:Ax= Ayf:C \to \sum_{x:A} \sum_{y:A} x =_A y

into the type of all identity types in AA, and given a function c:ACc:A \to C and a homotopy

p: x:Af(c(x))= x:A y:Ax= AyΔ A(x)p:\prod_{x:A} f(c(x)) =_{\sum_{x:A} \sum_{y:A} x =_A y} \Delta_A(x)

which states that the composite of ff and cc is the diagonal, one can construct

  • a function
g:( x:A y:Ax= Ay)Cg:\left(\sum_{x:A} \sum_{y:A} x =_A y\right) \to C
  • a homotopy witnessing that gg is a section of ff:
sec g: z: x:A y:Ax= Ayf(g(z))= x:A y:Ax= Ayz\mathrm{sec}_g:\prod_{z:\sum_{x:A} \sum_{y:A} x =_A y} f(g(z)) =_{\sum_{x:A} \sum_{y:A} x =_A y} z

such that for all x:Ax:A, g(Δ A(x))c(x)g(\Delta_A(x)) \equiv c(x) and sec g(Δ A(x))p(x)\mathrm{sec}_g(\Delta_A(x)) \equiv p(x).

By currying this is the same as saying that one can construct

  • a family of functions
g: x:A y:A(x= Ay)Cg:\prod_{x:A} \prod_{y:A} (x =_A y) \to C
  • a family of functions:
sec g: x:A y:A p:x= Ayf(g(x,y,p))= x:A y:Ax= Ay(x,y,p)\mathrm{sec}_g:\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} f(g(x, y, p)) =_{\sum_{x:A} \sum_{y:A} x =_A y} (x, y, p)

such that for all x:Ax:A, g(x,x,refl A(x))c(x)g(x, x, \mathrm{refl}_A(x)) \equiv c(x) and sec g(x,x,refl A(x))p(x)\mathrm{sec}_g(x, x, \mathrm{refl}_A(x)) \equiv p(x).

In terms of inductive types

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 AA is inductively generated by reflexivity x=xx = 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 xx is a parameter of the inductive definition rather than an index. In other words, the first definition says “for each type AA, we have a type Id AId_A dependent on A×AA\times A, inductively defined by a constructor idpathidpath which takes an element x:Ax\colon A as input and yields output in Id A(x,x)Id_A(x,x)” while the second definition says “for each type AA and each element x:Ax\colon A, we have a type Id A(x)Id_A(x) dependent on AA, inductively defined by a constructor idpathidpath which takes no input and yields output in Id A(x)(x)Id_A(x)(x).” The two formulations can be proven equivalent, but sometimes one is more convenient than the other.

η\eta-conversion and the reflection rule

Almost all types in type theory can be given both beta-reduction and eta-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:

Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)C(x,y,p):TypeΓ,x:A,y:A,p:Id A(x,y),Δ(x,x,r(x))t:C(x,y,p)Γ,x:A,y:A,p:Id A(x,y),Δ(x,y,p)J(t[x/y,r(x)/p];x,y,p)=t\frac{\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash C(x,y,p):Type \qquad \Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,x,r(x)) \vdash t : C(x,y,p)} {\Gamma, x:A, y:A, p:Id_A(x,y), \Delta(x,y,p) \vdash J(t[x/y, r(x)/p];x,y,p) = t}

This says that if CC is a type which we can use the eliminator JJ to construct a term of, but we already have a term tt of that type, then if we restrict tt to reflexivity inputs and then apply JJ to construct a term of type CC, the result is the same as the term tt we started with. As in the β\beta-reduction rule, the == in the conclusion refers to judgmental equality.

This η\eta-conversion rule has some very strong consequences. For instance, suppose x:Ax\colon A, y:Ay\colon A, and p:Id A(x,y)p\colon Id_A(x,y), and let CAC \coloneqq A. Then with t=xt=x, the η\eta-conversion rule tells us that x=J(x[x/y,r(x)/p];x,y,p)x = J(x[x/y,r(x)/p];x,y,p). And with t=yt=y, the η\eta-conversion rule tells us that y=J(y[x/y,r(x)/p];x,y,p)y = J(y[x/y,r(x)/p];x,y,p). But substituting xx for yy (and r(x)r(x) for pp) in the term yy simply yields the term xx, which is the same as the result of substituting xx for yy and r(x)r(x) for pp in the term xx. Thus, we have

x=J(x;x,y,p)=yx = J(x;x,y,p) = y

In other words, if Id A(x,y)Id_A(x,y) is inhabited (that is, xx and yy are typally equal) then in fact xx and yy are judgmentally equal. Moreover, by a similar argument we can show that

p=J(p[x/y,r(x)/p];x,y,p)=J(r(x)[x/y,r(x)/p];x,y,p)=r(x).p = J(p[x/y, r(x)/p];x,y,p) = J(r(x)[x/y,r(x)/p];x,y,p) = r(x).

(Here we are eliminating into the type C(x,y,p)Id A(x,y)C(x,y,p) \coloneqq Id_A(x,y). The term r(x)r(x) may be regarded as belonging to this type, because we have already shown that xx and yy are judgmentally equal.)

Thus, the judgmental η\eta-conversion rule for identity types implies the “reflection rule” for identity types, which in turn implies that the type theory is set-level. (This was observed already in (Streicher).) In particular, in homotopy type theory we cannot assume the η\eta-conversion rule for identity types.

However, the reflection rule for identity types is also problematic for non-homotopical reasons: since type-checking in dependent type theory depends on judgmental equality, but the above rule implies that judgmental equality depends on inhabitation of identity types, this makes judgmental equality and hence type-checking undecidable in the formal computational sense. Thus, η\eta-conversion for identity types is often omitted even in set-level type theories (e.g. Coq and Agda).

On the other hand, it is possible to prove a typal version of η\eta-conversion using only the identity types as defined above without judgmental η\eta-conversion. In other words, given the hypotheses of the above η\eta-conversion rule, we can construct a term belonging to the type

Id C(x,y,p)(J(t[x/y,r(x)/p];x,y,p),t). Id_{C(x,y,p)}(J(t[x/y, r(x)/p];x,y,p), t).

This has none of the bad consequences of judgmental η\eta-conversion, and in particular does not imply that the type theory is extensional. The argument that p:Id A(x,y)p\colon Id_A(x,y) implies x=yx=y becomes the tautologous statement that if p:Id A(x,y)p\colon Id_A(x,y) then p:Id A(x,y)p\colon Id_A(x,y), while the subsequent argument that p=r(x)p= r(x) fails because xx and yy are no longer judgmentally equal, so r(x)r(x) does not have type Id A(x,y)Id_A(x,y). We can transport it along pp to obtain a term of this type, but then we obtain only that pp is equal to the transport of r(x)r(x) along pp, which is a perfectly intensional/homotopical statement.

Dependent universal property

The identity types in Martin-Löf type theory satisfy the typal β\beta-conversion and typal η\eta-conversion rules, regardless if the original β\beta-conversion and η\eta-conversion rules used typal equality or judgmental equality. The elimination rule in conjunction with the typal β\beta-conversion and typal η\eta-conversion rules state that identity types satisfy the dependent universal property of identity types. If the dependent type theory also has dependent sum types product types, dependent product types, and dependent function types, allowing one to define the uniqueness quantifier, the dependent universal property of the natural numbers can be simplified to the following rule:

Γ,x:A,y:A,p:Id A(x,y)C(x,y,p)typeΓt: c:AC(c,c,Id A(c))Γa:AΓup Id A(t,a):!J:( c:AC(c,c,id A(c)))( x:A y:A p:Id A(x,y)C(x,y,p)).Id C(a,a,id A(a))(J(t,a,a,id A(a)),t(a)) \frac{\Gamma, x:A, y:A, p:\mathrm{Id}_A(x, y) \vdash C(x, y, p) \; \mathrm{type} \quad \Gamma \vdash t:\prod_{c:A} C(c, c, \mathrm{Id}_A(c)) \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{up}_{\mathrm{Id}_A}(t, a):\exists!J:\left(\prod_{c:A} C(c, c, \mathrm{id}_A(c))\right) \to \left(\prod_{x:A} \prod_{y:A} \prod_{p:\mathrm{Id}_A(x, y)} C(x, y, p)\right).\mathrm{Id}_{C(a, a, \mathrm{id}_A(a))}(J(t, a, a, \mathrm{id}_A(a)), t(a))}

 Variants of the identity type

Given a type AA, two elements x:Ax:A and y:Ay:A is equivalently

  • a function rec 𝟚 A(x,y):𝟚A\mathrm{rec}_\mathbb{2}^A(x, y):\mathbb{2} \to A from 𝟚\mathbb{2} to AA by the recursion and uniqueness principle of the boolean domain 𝟚\mathbb{2},

  • a pair in(x,y):A×A\mathrm{in}(x, y):A \times A by the introduction rule of pair types A×AA \times A.

From the other side, a function f:𝟚Af:\mathbb{2} \to A is equivalently two elements f(0):Af(0):A and f(1):Af(1):A, and by the negative recursion and uniqueness rules of pair types, a pair z:A×Az:A \times A is equivalently two elements π 1(z):A\pi_1(z):A and π 2(z)\pi_2(z). This implies that one can define two variants of the identity type,

  • a variant Id A(f)\mathrm{Id}_A(f) indexed by functions f:𝟚Af:\mathbb{2} \to A out of the boolean domain, where the usual identity type is then defined as

    x= AyId A(rec 𝟚 A(x,y))x =_A y \coloneqq \mathrm{Id}_A(\mathrm{rec}_\mathbb{2}^A(x, y))
  • a variant Id A(z)\mathrm{Id}_A(z) indexed by pairs z:A×Az:A \times A, where the usual identity type is then defined as

    x= AyId A(in(x,y))x =_A y \coloneqq \mathrm{Id}_A(\mathrm{in}(x, y))

Identity types indexed by functions from the booleans

The inference rules for identity types indexed by functions from the booleans is given as follows:

First the rule that defines the identity type itself, as a dependent type, in some context Γ\Gamma.

type formation

ΓA:TypeΓ,f:𝟚AId A(f):Type\frac{\Gamma \vdash A:Type}{\Gamma, f:\mathbb{2} \to A \vdash Id_A(f):Type}

Now the basic “introduction” rule, which says that the elements of AA encoded in the constant function λb:𝟚.x\lambda b:\mathbb{2}.x which sends every boolean b:𝟚b:\mathbb{2} to x:Ax:A are equal in a canonical way.

term introduction

ΓA:TypeΓ,x:Ar(x):Id A(λb:𝟚.x)\frac{\Gamma \vdash A:Type}{\Gamma, x:A \vdash r(x) : Id_A(\lambda b:\mathbb{2}.x)}

Then we have the “elimination” rule:

Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓ,x:A,Δ(λb:𝟚.x,r(x))t(x):C(λb:𝟚.x,r(x))Γ,f:𝟚A,p:Id A(f)J ̲.t(f,p):C(f,p)\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \quad \Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash t(x):C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, f:\mathbb{2} \to A, p:Id_A(f) \vdash J^{\underline{ }.t}(f,p) : C(f,p)}

The elimination rule then says that if:

  1. for any f:𝟚Af:\mathbb{2} \to A and any reason p:Id A(f)p:Id_A(f) why the two elements of AA encoded in the functions are the same, we have a type C(f,p)C(f,p)
  2. for any x:Ax:A we have a t(x):C(λb:𝟚.x,r(x))t(x):C(\lambda b:\mathbb{2}.x,r(x)),

we can construct a canonically defined term J ̲.t(f,p):C(f,p)J^{\underline{ }.t}(f,p):C(f,p) for any ff and p:Id A(f)p:Id_A(f), by “transporting” the family of terms t(x)t(x) dependent upon the element x:Ax:A along the proof of equality pp. The elimination rule alternatively says that in order to prove a statement is true about all f,pf,p, it suffices to prove it in the special case for λb:𝟚.x,r(x)\lambda b:\mathbb{2}.x,r(x).

Finally, we have the “computation” or beta-reduction rule. There are two possible computation rules, which result in strict and weak identity types respectively. The computation rule for strict identity types says that if we substitute along a reflexivity proof, nothing happens.

computation rule for strict identity types

Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓ,x:A,Δ(λb:𝟚.x,r(x))t(x):C(λb:𝟚.x,r(x))Γ,x:A,Δ(λb:𝟚.x,r(x))J ̲.t(λb:𝟚.x,r(x))=t(x)\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \quad \Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash t(x):C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash J^{\underline{ }.t}(\lambda b:\mathbb{2}.x,r(x)) = t(x)}

Note that the equality == in the conclusion of this computation rule is judgmental equality, not an instance of the identity/equality type itself.

The computation rule for weak identity types says that there is a witness that the substitution along a reflexivity proof is equal to the original t(x)t(x).

computation rule for weak identity types

Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓ,x:A,Δ(λb:𝟚.x,r(x))t(x):C(λb:𝟚.x,r(x))Γ,x:A,Δ(λb:𝟚.x,r(x))β ̲.t(x):Id C(λb:𝟚.x,r(x))(J ̲.t(λb:𝟚.x,r(x)),t(x))\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \quad \Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash t(x):C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash \beta^{\underline{ }.t}(x):Id_{C(\lambda b:\mathbb{2}.x,r(x))}(J^{\underline{ }.t}(\lambda b:\mathbb{2}.x,r(x)),t(x))}

If we have dependent product types, we can directly use the dependent function Γt: x:AC(λb:𝟚.x,r(x))\Gamma \vdash t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x)) instead of the family of terms t(x)t(x) dependent upon x:Ax:A in the hypothesis. Then the canonically defined term is given by J(t,f,p):C(f,p)J(t,f,p):C(f,p) and is dependent upon dependent function t: x:AC(λb:𝟚.x,r(x))t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x)) rather than annotated with the family t(x)t(x).

Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓt: x:AC(λb:𝟚.x,r(x))Γ,f:𝟚A,p:Id A(f)J(t,f,p):C(f,p)\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, f:\mathbb{2} \to A, p:Id_A(f) \vdash J(t,f,p) : C(f,p)}
Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓt: x:AC(λb:𝟚.x,r(x))Γ,x:A,Δ(λb:𝟚.x,r(x))J(t,λb:𝟚.x,r(x))=t(x)\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash J(t,\lambda b:\mathbb{2}.x,r(x)) = t(x)}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by J(λx:A.t(x),f,p):C(f,p)J(\lambda x:A.t(x),f,p):C(f,p) and J(λx:A.t(x),λb:𝟚.x,r(x))t(x):C(λb:𝟚.x,r(x))J(\lambda x:A.t(x),\lambda b:\mathbb{2}.x,r(x)) \equiv t(x):C(\lambda b:\mathbb{2}.x,r(x)). .

Similarly, the canonically defined term in the propositional computation rule is given by the identification β(t,x):Id C(λb:𝟚.x,r(x))(J(t,λb:𝟚.x,r(x)),t(x))\beta(t,x):Id_{C(\lambda b:\mathbb{2}.x,r(x))}(J(t,\lambda b:\mathbb{2}.x,r(x)),t(x)) and is dependent upon dependent function t: x:AC(λb:𝟚.x,r(x))t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x)) rather than annotated with the family t(x)t(x).

Γ,f:𝟚A,p:Id A(f),Δ(f,p)C(f,p):TypeΓt: x:AC(λb:𝟚.x,r(x))Γ,x:A,Δ(λb:𝟚.x,r(x))β(t,x):Id C(λb:𝟚.x,r(x))(J(t,λb:𝟚.x,r(x)),t(x))\frac{\Gamma, f:\mathbb{2} \to A, p:Id_A(f), \Delta(f,p) \vdash C(f,p):Type \qquad \Gamma \vdash t:\prod_{x:A} C(\lambda b:\mathbb{2}.x,r(x))} {\Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash \beta(t,x):Id_{C(\lambda b:\mathbb{2}.x,r(x))}(J(t,\lambda b:\mathbb{2}.x,r(x)),t(x))}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by β(λx:A.t(x),x):Id C(λb:𝟚.x,r(x))(J(λx:A.t(x),λb:𝟚.x,r(x)),t(x))\beta(\lambda x:A.t(x),x):\mathrm{Id}_{C(\lambda b:\mathbb{2}.x,r(x))}(J(\lambda x:A.t(x),\lambda b:\mathbb{2}.x,r(x)),t(x)).

Identity types indexed by pairs

The inference rules for identity types indexed by pairs is given as follows:

First the rule that defines the identity type itself, as a dependent type, in some context Γ\Gamma.

type formation

ΓA:TypeΓ,z:A×AId A(z):Type\frac{\Gamma \vdash A:Type}{\Gamma, z:A \times A \vdash Id_A(z):Type}

Now the basic “introduction” rule, which says that the elements encoded in the non-dependent diagonal Δ A(x)λx:A.(x,x)\Delta_A(x) \coloneqq \lambda x:A.(x, x) at x:Ax:A are equal in a canonical way.

term introduction

ΓA:TypeΓ,x:Ar(x):Id A(Δ A(x))\frac{\Gamma \vdash A:Type}{\Gamma, x:A \vdash r(x) : Id_A(\Delta_A(x))}

Then we have the “elimination” rule:

Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓ,x:A,Δ(Δ A(x),r(x))t(x):C(Δ A(x),r(x))Γ,z:A×A,p:Id A(z)J ̲.t(z,p):C(z,p)\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash t(x):C(\Delta_A(x),r(x))} {\Gamma, z:A \times A, p:Id_A(z) \vdash J^{\underline{ }.t}(z,p) : C(z,p)}

The elimination rule then says that if:

  1. for any z:A×Az:A \times A and any reason p:Id A(z)p:Id_A(z) why the two elements of AA encoded in the pair are the same, we have a type C(z,p)C(z,p)
  2. for any x:Ax:A we have a t(x):C(Δ A(x),r(x))t(x):C(\Delta_A(x),r(x)),

we can construct a canonically defined term J ̲.t(z,p):C(z,p)J^{\underline{ }.t}(z,p):C(z,p) for any zz and p:Id A(z)p:Id_A(z), by “transporting” the family of terms t(x)t(x) dependent upon the element x:Ax:A along the proof of equality pp. The elimination rule alternatively says that in order to prove a statement is true about all z,pz,p, it suffices to prove it in the special case for Δ A(x),r(x)\Delta_A(x),r(x).

Finally, we have the “computation” or beta-reduction rule. There are two possible computation rules, which result in strict and weak identity types respectively. The computation rule for strict identity types says that if we substitute along a reflexivity proof, nothing happens.

computation rule for strict identity types

Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓ,x:A,Δ(Δ A(x),r(x))t(x):C(Δ A(x),r(x))Γ,x:A,Δ(Δ A(x),r(x))J ̲.t(Δ A(x),r(x))=t(x)\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash t(x):C(\Delta_A(x),r(x))} {\Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash J^{\underline{ }.t}(\Delta_A(x),r(x)) = t(x)}

Note that the equality == in the conclusion of this computation rule is judgmental equality, not an instance of the identity/equality type itself.

The computation rule for weak identity types says that there is a witness that the substitution along a reflexivity proof is equal to the original t(x)t(x).

computation rule for weak identity types

Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓ,x:A,Δ(Δ A(x),r(x))t(x):C(Δ A(x),r(x))Γ,x:A,Δ(Δ A(x),r(x))β ̲.t(x):Id C(Δ A(x),r(x))(J ̲.t(Δ A(x),r(x)),t(x))\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash t(x):C(\Delta_A(x),r(x))} {\Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash \beta^{\underline{ }.t}(x):Id_{C(\Delta_A(x),r(x))}(J^{\underline{ }.t}(\Delta_A(x),r(x)),t(x))}

If we have dependent product types, we can directly use the dependent function Γt: x:AC(Δ A(x),r(x))\Gamma \vdash t:\prod_{x:A} C(\Delta_A(x),r(x)) instead of the family of terms t(x)t(x) dependent upon x:Ax:A in the hypothesis. Then the canonically defined term is given by J(t,z,p):C(z,p)J(t,z,p):C(z,p) and is dependent upon dependent function t: x:AC(Δ A(x),r(x))t:\prod_{x:A} C(\Delta_A(x),r(x)) rather than annotated with the family t(x)t(x).

Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓt: x:AC(Δ A(x),r(x))Γ,z:A×A,p:Id A(z)J(t,z,p):C(z,p)\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(\Delta_A(x),r(x))} {\Gamma, z:A \times A, p:Id_A(z) \vdash J(t,z,p) : C(z,p)}
Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓt: x:AC(Δ A(x),r(x))Γ,x:A,Δ(Δ A(x),r(x))J(t,Δ A(x),r(x))=t(x)\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(\Delta_A(x),r(x))} {\Gamma, x:A, \Delta(\Delta_A(x),r(x)) \vdash J(t,\Delta_A(x),r(x)) = t(x)}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by J(λx:A.t(x),z,p):C(z,p)J(\lambda x:A.t(x),z,p):C(z,p) and J(λx:A.t(x),Δ A(x),r(x))t(x):C(Δ A(x),r(x))J(\lambda x:A.t(x),\Delta_A(x),r(x)) \equiv t(x):C(\Delta_A(x),r(x)). .

Similarly, the canonically defined term in the propositional computation rule is given by the identification β(t,x):Id C(Δ A(x),r(x))(J(t,Δ A(x),r(x)),t(x))\beta(t,x):Id_{C(\Delta_A(x),r(x))}(J(t,\Delta_A(x),r(x)),t(x)) and is dependent upon dependent function t: x:AC(Δ A(x),r(x))t:\prod_{x:A} C(\Delta_A(x),r(x)) rather than annotated with the family t(x)t(x).

Γ,z:A×A,p:Id A(z),Δ(z,p)C(z,p):TypeΓt: x:AC(Δ A(x),r(x))Γ,x:A,Δ(λb:𝟚.x,r(x))β(t,x):Id C(λb:𝟚.x,r(x))(J(t,λb:𝟚.x,r(x)),t(x))\frac{\Gamma, z:A \times A, p:Id_A(z), \Delta(z,p) \vdash C(z,p):Type \quad \Gamma \vdash t:\prod_{x:A} C(\Delta_A(x),r(x))} {\Gamma, x:A, \Delta(\lambda b:\mathbb{2}.x,r(x)) \vdash \beta(t,x):Id_{C(\lambda b:\mathbb{2}.x,r(x))}(J(t,\lambda b:\mathbb{2}.x,r(x)),t(x))}

The original inference rules using the family of terms t(x)t(x) dependent upon x:Ax:A is then given by β(λx:A.t(x),x):Id C(Δ A(x),r(x))(J(λx:A.t(x),Δ A(x),r(x)),t(x))\beta(\lambda x:A.t(x),x):\mathrm{Id}_{C(\Delta_A(x),r(x))}(J(\lambda x:A.t(x),\Delta_A(x),r(x)),t(x)).

Definition from an interval type

Suppose that one has an interval type 𝕀\mathbb{I}, with elements 0:𝕀0:\mathbb{I} and 1:𝕀1:\mathbb{I}.

ΓctxΓ𝕀type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{I} \; \mathrm{type}}
ΓctxΓ0:𝕀ΓctxΓ1:𝕀\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{I}} \quad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathbb{I}}

Usually, the recursion principle of the interval type is interpreted as a way to construct, from elements x:Ax:A and y:Ay:A and identification p:x= Ayp:x =_A y, paths p:𝕀Ap:\mathbb{I} \to A, aka functions from the interval type to AA. Interpreted another way, the recursion principle of the interval type are the negative elimination and computation rules for identity types, allowing one to define identity types as negative types. Thus, these identity types can be called negative identity types, in contrast to the Martin-Löf identity types, which can be called positive identity types.

Inference rules

  • The formation rule of identity types state that given a type AA and elements x:Ax:A and y:Ay:A, one can form the identity type x= Ayx =_A y. Syntactically, this is given by the following inference rules:
ΓAtypeΓ,x:A,y:Ax= Aytype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A, y:A \vdash x =_A y \; \mathrm{type}}
  • The introduction rule of identity types state that given a type AA and a path p:𝕀Ap:\mathbb{I} \to A, one can construct an identification toId A(f):f(0)= Af(1)\mathrm{toId}_A(f):f(0) =_A f(1). Syntactically, this is given by the following inference rules:
ΓAtypeΓf:𝕀AΓtoId A(f):f(0)= Af(1)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{toId}_A(f):f(0) =_A f(1)}

Normally, this would be function application to the canonical identification 𝓅:0= 𝕀1\mathcal{p}:0 =_\mathbb{I} 1, but here we haven’t defined 𝓅\mathcal{p} yet since we haven’t defined the identity type yet, and with this rule one can define said identification to be the identification of the identity function on the interval type

𝓅toId 𝕀(id 𝕀):0= 𝕀1\mathcal{p} \equiv \mathrm{toId}_\mathbb{I}(\mathrm{id}_\mathbb{I}):0 =_\mathbb{I} 1

In addition, reflexivity of an element x:Ax:A is given by sending the constant path of x:Ax:A to its equality

refl A(x)toId A(λi:𝕀.x):x= Ax\mathrm{refl}_A(x) \equiv \mathrm{toId}_{A}(\lambda i:\mathbb{I}.x):x =_A x
  • The elimination rule of identity types state that given a type AA, elements x:Ax:A and y:Ay:A, and identification p:x= Ayp:x =_A y, one can construct a path topath 𝕀 A(x,y,p):𝕀A\mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A. Syntactically, this is given by the following inference rules:
ΓAtypeΓx:AΓy:AΓp:x= AyΓtopath 𝕀 A(x,y,p):𝕀A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A}

This is just another name for the recursor of the interval type rec 𝕀 A(x,y,p):𝕀A\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A.

  • The three computation rules of identity types state that given a type AA, elements x:Ax:A and y:Ay:A, and identification p:x= Ayp:x =_A y,
    topath 𝕀 A(x,y,p)(0)xtopath 𝕀 A(x,y,p)(1)ytoId A(topath 𝕀 A(x,y,p))p\mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x \quad \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y \quad \mathrm{toId}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p

    Syntactically, this is given by the following inference rules:

ΓAtypeΓx:AΓy:AΓp:x= AyΓtopath 𝕀 A(x,y,p)(0)x:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(0) \equiv x:A}
ΓAtypeΓx:AΓy:AΓp:x= AyΓtopath 𝕀 A(x,y,p)(1)y:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(x, y, p)(1) \equiv y:A}
ΓAtypeΓx:AΓy:AΓp:x= AyΓtoId A(topath 𝕀 A(x,y,p))p:x= Ay\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A \quad \Gamma \vdash y:A \quad \Gamma \vdash p:x =_A y}{\Gamma \vdash \mathrm{toId}_{A}(\mathrm{topath}_\mathbb{I}^A(x, y, p)) \equiv p:x =_A y}
  • The uniqueness rule of identity types state that given a type AA and a path p:𝕀Ap:\mathbb{I} \to A,
    topath 𝕀 A(p(0),p(1),toId A(p))p\mathrm{topath}_\mathbb{I}^A(p(0), p(1), \mathrm{toId}_A(p)) \equiv p

Syntactically, this is given by the following inference rules:

ΓAtypeΓf:𝕀AΓtopath 𝕀 A(f(0),f(1),toId A(f))f:𝕀A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash f:\mathbb{I} \to A}{\Gamma \vdash \mathrm{topath}_\mathbb{I}^A(f(0), f(1), \mathrm{toId}_A(f)) \equiv f:\mathbb{I} \to A}

Path induction

The associated path induction rule then says that the function type 𝕀A\mathbb{I} \to A is a positive copy of AA:

ΓAtypeΓ,z:𝕀AC(z)typet: x:AC(λi:𝕀.x)Γind 𝕀A(t): z:𝕀AC(z)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \; \mathrm{type} \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma \vdash \mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z)}
ΓAtypeΓ,z:𝕀AC(z)typet: x:AC(λi:𝕀.x)Γ,x:Aind 𝕀A(t,λi:𝕀.x)t(x):C(λi:𝕀.x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, z:\mathbb{I} \to A \vdash C(z) \; \mathrm{type} \quad t:\prod_{x:A} C(\lambda i:\mathbb{I}.x)}{\Gamma, x:A \vdash \mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x)}

Theorem

Suppose that path induction for function types out of the interval type is true. Then the J-rule is true: given a type AA and given a type family C(x,y,p)C(x, y, p) indexed by x:Ax:A, y:Ay:A, and p:x= Ayp:x =_A y, and a dependent function t: x:AC(x,x,refl A(x))t:\prod_{x:A} C(x, x, \mathrm{refl}_A(x)), one can construct a dependent function

ind =,A(t): x:A y:A p:x= AyC(x,y,p)\mathrm{ind}_{=, A}(t):\prod_{x:A} \prod_{y:A} \prod_{p:x =_A y} C(x, y, p)

such that for all x:Ax:A,

J(t,x,x,refl A(x))t(x)J(t, x, x, \mathrm{refl}_A(x)) \equiv t(x)

Proof

By path induction on the type family C(f(0),f(1),toId A(f))C(f(0), f(1), \mathrm{toId}_A(f)) indexed by f:𝕀Af:\mathbb{I} \to A, we can construct a dependent function

ind 𝕀A(t): f:𝕀AC(f(0),f(1),toId A(f))\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{f:\mathbb{I} \to A} C(f(0), f(1), \mathrm{toId}_A(f))

such that for all x:Ax:A,

ind 𝕀A(t,λi:𝕀.x)t(x):C(λi:𝕀.x)\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x)

since by definition of constant function and reflexivity, one has

(λi:𝕀.x)(0)x(λi:𝕀.x)(1)xap λi:𝕀.x(𝓅)refl A(x)(\lambda i:\mathbb{I}.x)(0) \equiv x \quad (\lambda i:\mathbb{I}.x)(1) \equiv x \quad \mathrm{ap}_{\lambda i:\mathbb{I}.x}(\mathcal{p}) \equiv \mathrm{refl}_A(x)

We define

J(t,x,y,p)ind 𝕀A(t,rec 𝕀 A(x,y,p))J(t, x, y, p) \equiv \mathrm{ind}_{\mathbb{I} \to A}(t, \mathrm{rec}_\mathbb{I}^A(x, y, p))

since by interval recursion one has a path rec 𝕀 A(x,y,p):𝕀A\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A such that

rec 𝕀 A(x,y,p)(0)xrec 𝕀 A(x,y,p)(1)yap rec 𝕀 A(x,y,p)(0,1,𝓅)p\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x \quad \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y \quad \mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}(0, 1, \mathcal{p}) \equiv p

Alternatively, one can say that 𝕀A\mathbb{I} \to A is a negative copy of AA with respect to constant functions, or equivalently that every type AA is definitionally I\mathrm{I}-local, or that

const A,𝕀λx:A.λi:𝕀.x:A(𝕀A)\mathrm{const}_{A, \mathbb{I}} \equiv \lambda x:A.\lambda i:\mathbb{I}.x:A \to (\mathbb{I} \to A)

is a definitional isomorphism:

ΓAtypeΓ,p:𝕀Aconst A,I 1(p):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \mathrm{const}_{A, \mathrm{I}}^{-1}(p):A}
ΓAtypeΓ,x:Aconst A,I 1(λi:𝕀.x)x:A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:A \vdash \mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) \equiv x:A}
ΓAtypeΓ,p:𝕀Aλi:𝕀.const A,I 1(p)p:𝕀A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathbb{I} \to A \vdash \lambda i:\mathbb{I}.\mathrm{const}_{A, \mathrm{I}}^{-1}(p) \equiv p:\mathbb{I} \to A}

This is called definitional interval type localization.

Then, one can prove path induction (positive copy induction rules):

Theorem

Suppose that every type AA is definitionally 𝕀\mathbb{I}-local.

Then path induction holds: given any type AA, and any type family C(p)C(p) indexed by paths p:𝕀Ap:\mathbb{I} \to A in AA, and given any dependent function t: x:AC(λi:𝕀.x)t:\prod_{x:A} C(\lambda i:\mathbb{I}.x) which says that for all elements x:Ax:A, there is an element of the type defined by substituting the constant path of x:Ax:A into CC, C(λi:𝕀.x)C(\lambda i:\mathbb{I}.x), one can construct a dependent function ind 𝕀A(t): z:𝕀AC(z)\mathrm{ind}_{\mathbb{I} \to A}(t):\prod_{z:\mathbb{I} \to A} C(z) such that for all x:Ax:A, ind 𝕀A(t,λi:𝕀.x)t(x):C(λi:𝕀.x)\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(x):C(\lambda i:\mathbb{I}.x).

Proof

ind 𝕀A(t)\mathrm{ind}_{\mathbb{I} \to A}(t) is defined to be

ind 𝕀A(t)λp:𝕀A.t(const A,I 1(p))\mathrm{ind}_{\mathbb{I} \to A}(t) \equiv \lambda p:\mathbb{I} \to A.t(\mathrm{const}_{A, \mathrm{I}}^{-1}(p))

and by the computation rules of path types as negative copies, one has that for all x:Ax:A,

const A,I 1(λi:𝕀.x)x\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x) \equiv x

and so by definition of ind 𝕀A(t)\mathrm{ind}_{\mathbb{I} \to A}(t) and the judgmental congruence rules for substitution, one has

ind 𝕀A(t,λi:𝕀.x)t(const A,I 1(λi:𝕀.x))t(x)\mathrm{ind}_{\mathbb{I} \to A}(t, \lambda i:\mathbb{I}.x) \equiv t(\mathrm{const}_{A, \mathrm{I}}^{-1}(\lambda i:\mathbb{I}.x)) \equiv t(x)

Thus, everything about identity types in Martin-Löf type theory could be proven in this theory.

On the other hand, propositional interval type localization, which says that

const A,𝕀λx:A.λi:𝕀.x:A(𝕀A)\mathrm{const}_{A, \mathbb{I}} \equiv \lambda x:A.\lambda i:\mathbb{I}.x:A \to (\mathbb{I} \to A)

is a weak equivalence of types, only implies the propositional J-rule.

One has the following analogies between localization at a specific type and the type theoretic letter rule that it proves:

localization ruletype theoretic letter rule
𝕀 \mathbb{I} -localizationJ-rule
S 1 S^1 -localizationK-rule

Kan operations

Defining identity types in terms of an interval type gives the type theory a cubical flavor, although here the interval 𝕀\mathbb{I} is an actual type, rather than a pretype in cubical type theory. In particular, one can use path induction to construct the Kan operations. The following proofs are adapted from Bentzen2019.

Theorem

Given paths f:𝕀Af:\mathbb{I} \to A and g:𝕀Ag:\mathbb{I} \to A, one can construct a function

fill A(f,g):(f(0)= Ag(0))(f(1)= Ag(1))\mathrm{fill}_A(f, g):(f(0) =_A g(0)) \to (f(1) =_A g(1))

This is defined by double path induction by sending the constant path of xx in each parameter to its filler of identifications, which is just the identity function on x= Axx =_A x

x:Afill A(λi:𝕀.x,λi:𝕀.x)id x= Ax:(x= Ax)(x= Ax)x:A \vdash \mathrm{fill}_A(\lambda i:\mathbb{I}.x, \lambda i:\mathbb{I}.x) \equiv \mathrm{id}_{x =_A x}:(x =_A x) \to (x =_A x)

Theorem

Given elements x:Ax:A, y:Ay:A and identification p:x= Ayp:x =_A y, one can construct the inverse identification p 1:(y= Ax)p^{-1}:(y =_A x).

By interval recursion, there are paths rec 𝕀 A(x,y,p):𝕀A\mathrm{rec}_\mathbb{I}^A(x, y, p):\mathbb{I} \to A. By evaluating the fillers of the recursively defined path and the identity path on xx at reflexivity of xx, one gets the needed identity:

p 1fill A(rec 𝕀 A(x,y,p),λi:𝕀.x,refl A(y)):(y= Ax)p^{-1} \equiv \mathrm{fill}_A(\mathrm{rec}_\mathbb{I}^A(x, y, p), \lambda i:\mathbb{I}.x, \mathrm{refl}_A(y)):(y =_A x)
x =refl A(x) x p refl A(x) y =p 1 x \begin{array}{ccccc} & x & \overset{\mathrm{refl}_A(x)}= & x & \\ p & \Vert & & \Vert & \mathrm{refl}_A(x) \\ & y & \underset{p^{-1}}= & x & \\ \end{array}

Theorem

Given elements x:Ax:A, y:Ay:A, z:Az:A and identifications p:x= Ayp:x =_A y and q:y= Azq:y =_A z, one can construct an identification pq:(x= Az)p \bullet q:(x =_A z) called the concatenation of pp and qq.

By interval recursion, there is a path rec 𝕀 A(y,z,q):𝕀A\mathrm{rec}_\mathbb{I}^A(y, z, q):\mathbb{I} \to A. By evaluating the fillers of the constant path of xx and the path of qq at pp, one gets the needed identification:

pqfill A(λi:𝕀.x,rec 𝕀 A(y,z,q),p):(x= Az)p \bullet q \equiv \mathrm{fill}_A(\lambda i:\mathbb{I}.x, \mathrm{rec}_\mathbb{I}^A(y, z, q), p):(x =_A z)
x =p y refl A(x) q x =pq z \begin{array}{ccccc} & x & \overset{p}= & y & \\ \mathrm{refl}_A(x) & \Vert & & \Vert & q \\ & x & \underset{p \bullet q}= & z & \\ \end{array}

Other properties

There are other things which can be defined similarly to cubical type theory. For example, function extensionality is provable:

Theorem

Given dependent functions f: x:AB(x)f:\prod_{x:A} B(x) and g: x:AB(x)g:\prod_{x:A} B(x) and a homotopy H: x:Af(x)= B(x)g(x)H:\prod_{x:A} f(x) =_{B(x)} g(x), we have an identification funext(f,g,H):f= x:AB(x)g\mathrm{funext}(f, g, H):f =_{\prod_{x:A} B(x)} g

Proof

This is defined by

funext(f,g,H)toId x:AB(x)(λi:𝕀.λx:A.topath 𝕀 B(x)(f(x),g(x),H(x))(i))\mathrm{funext}(f, g, H) \equiv \mathrm{toId}_{\prod_{x:A} B(x)}(\lambda i:\mathbb{I}.\lambda x:A.\mathrm{topath}_\mathbb{I}^{B(x)}(f(x), g(x), H(x))(i))

Similarly, function application to identifications can be defined without the use of path induction:

Theorem

Given types AA and BB, a a function f:ABf:A \to B, elements x:Ax:A and y:Ay:A and an identification p:x= Ayp:x =_A y, one can construct the identification ap f(x,y,p):f(x)= Bf(y)\mathrm{ap}_f(x, y, p):f(x) =_B f(y).

This is defined through the inference rules for identity types and function composition:

ap f(x,y,p)toId B(frec 𝕀 A(x,y,p)):f(x)= Bf(y)\mathrm{ap}_f(x, y, p) \equiv \mathrm{toId}_B(f \circ \mathrm{rec}_\mathbb{I}^A(x, y, p)):f(x) =_B f(y)

This is sufficient to prove the recursion and uniqueness rules for the interval type:

Theorem

The recursion principle of the interval type:

Given a type AA, elements x:Ax:A and y:Ay:A and equality p:x= Ayp:x =_{A} y, one can construct a function rec 𝕀 A(x,y,p):𝕀A\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p):\mathbb{I} \to A such that

rec 𝕀 A(x,y,p)(0)xrec 𝕀 A(x,y,p)(1)yap rec 𝕀 A(x,y,p) =(0,1,toId 𝕀(id 𝕀))p\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x \quad \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y \quad \mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}^{=}(0, 1, \mathrm{toId}_\mathbb{I}(\mathrm{id}_\mathbb{I})) \equiv p

Proof

We define

rec 𝕀 A()(x,y,p)topath 𝕀 A()(x,y,p)\mathrm{rec}_{\mathbb{I}}^{A(-)}(x, y, p) \equiv \mathrm{topath}_{\mathbb{I}}^{A(-)}(x, y, p)

That rec 𝕀 A(x,y,p)(0)x\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(0) \equiv x is given by the first computation rule of identity types and that rec 𝕀 A(x,y,p)(1)y\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)(1) \equiv y is given by the second computation rules of identity types. Finally, by definition of function application to identification and the uniqueness rule of identity types, one has the following reduction:

ap rec 𝕀 A(x,y,p)(0,1,toId A(id 𝕀))toId A(rec 𝕀 A(x,y,p)rec 𝕀 𝕀(0,1,toId 𝕀(id 𝕀)))toId A(rec 𝕀 A(x,y,p)id 𝕀)\mathrm{ap}_{\mathrm{rec}_\mathbb{I}^{A}(x, y, p)}(0, 1, \mathrm{toId}_A(\mathrm{id}_\mathbb{I})) \equiv \mathrm{toId}_A(\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p) \circ \mathrm{rec}_\mathbb{I}^\mathbb{I}(0, 1, \mathrm{toId}_\mathbb{I}(\mathrm{id}_\mathbb{I}))) \equiv \mathrm{toId}_A(\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p) \circ \mathrm{id}_\mathbb{I})

and by function composition and the third computation rule of identity types, one has the following reduction

toId A(rec 𝕀 A(x,y,p)id 𝕀)toId A(rec 𝕀 A(x,y,p))p\mathrm{toId}_A(\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p) \circ \mathrm{id}_\mathbb{I}) \equiv \mathrm{toId}_A(\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p)) \equiv p

Theorem

The uniqueness principle of the interval type:

Given a type AA, elements x:Ax:A and y:Ay:A and equality p:x= Ayp:x =_{A} y, and given a function f:𝕀Af:\mathbb{I} \to A such that

f(0)xf(1)yap f(0,1,toId 𝕀(id 𝕀))pf(0) \equiv x \quad f(1) \equiv y \quad \mathrm{ap}_{f}(0, 1, \mathrm{toId}_\mathbb{I}(\mathrm{id}_\mathbb{I})) \equiv p

one has that frec 𝕀 A(x,y,p)f \equiv \mathrm{rec}_{\mathbb{I}}^{A}(x, y, p).

Proof

By definition of the recursor of the interval type,

rec 𝕀 A(x,y,p)topath 𝕀 A()(x,y,p)\mathrm{rec}_{\mathbb{I}}^{A}(x, y, p) \equiv \mathrm{topath}_{\mathbb{I}}^{A(-)}(x, y, p)

and by the judgmental congruence rules for substitution, one has that

topath 𝕀 A()(x,y,p)topath 𝕀 A(f(0),f(1),toId A(f))\mathrm{topath}_{\mathbb{I}}^{A(-)}(x, y, p) \equiv \mathrm{topath}_\mathbb{I}^A(f(0), f(1), \mathrm{toId}_A(f))

and by the uniqueness rule for identity types, one has that

topath 𝕀 A(f(0),f(1),toId A(f))f\mathrm{topath}_\mathbb{I}^A(f(0), f(1), \mathrm{toId}_A(f)) \equiv f

The recursion and uniqueness principles of the interval type are in turn sufficient to prove the induction principle of the interval type.

Definition in observational type theory

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:

ΓA:TypeΓ,x:A,y:AId A(x,y):Type\frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A \vdash Id_A(x,y):Type}

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×BA \times B has the following computation rule:

Id A×B(s,t)Id A(π 1s,π 1t)×Id B(π 2s,π 2t)Id_{A \times B} (s, t) \equiv Id_A(\pi_1 s, \pi_1 t) \times Id_B (\pi_2 s, \pi_2 t)

For types in universes

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:

A:𝒰a:𝒯 𝒰(A)b:𝒯 𝒰(A)id A(a,b):𝒰\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}}

We define a general congruence term called ap

x:Af:Bp:id A(a,a )ap x.f(p):id B(f[a/x],f[a /x])\frac{x:A \vdash f:B \quad p:\mathrm{id}_A(a, a^{'})}{\mathrm{ap}_{x.f}(p):\mathrm{id}_B(f[a/x], f[a^{'}/x])}

and the reflexivity terms:

a:Arefl a:id A(a,a)\frac{a:A}{\mathrm{refl}_{a}:\mathrm{id}_A(a, a)}

and computation rules for identity functions

ap x.x(p)p\mathrm{ap}_{x.x}(p) \equiv p

and for constant functions yy

ap x.y(p)refl y\mathrm{ap}_{x.y}(p) \equiv \mathrm{refl}_{y}

Thus, ap is a higher dimensional explicit substitution. There are judgmental equalities

ap x.f(refl a)refl f[a/x]\mathrm{ap}_{x.f}(\mathrm{refl}_{a}) \equiv \mathrm{refl}_{f[a/x]}
ap y.g(ap x.f(p))ap x.g[f/y](p)\mathrm{ap}_{y.g}(\mathrm{ap}_{x.f}(p)) \equiv \mathrm{ap}_{x.g[f/y]}(p)
ap x.t(p)refl t\mathrm{ap}_{x.t}(p) \equiv \mathrm{refl}_{t}

for constant term tt.

For universes

Let A 𝒰BA \cong_\mathcal{U} B be the type of bijective correspondences between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}, and let id 𝒰(A,B)\mathrm{id}_\mathcal{U}(A, B) be the identity type between two terms of a universe A:𝒰A:\mathcal{U} and B:𝒰B:\mathcal{U}. Then there are rules

R:A 𝒰BΔ(R):id 𝒰(A,B)P:id 𝒰(A,B)(P):A 𝒰BR:A 𝒰B(Δ(R))R\frac{R:A \cong_\mathcal{U} B}{\Delta(R):\mathrm{id}_\mathcal{U}(A, B)} \qquad \frac{P:\mathrm{id}_\mathcal{U}(A, B)}{\nabla(P):A \cong_\mathcal{U} B} \qquad \frac{R:A \cong_\mathcal{U} B}{\nabla(\Delta(R)) \equiv R}

Identity types in universes and singleton contractibility

Given a term of a universe A:𝒰A:\mathcal{U}

id 𝒯 𝒰(A)π 1((refl A))\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)} \equiv \pi_1(\nabla(\mathrm{refl}_A))

with terms representing singleton contractibility.

π 1(π 2((refl A)): a:𝒯 𝒰(A)isContr( b:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_1(\pi_2(\nabla(\mathrm{refl}_A)):\prod_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)
π 2(π 2((refl A))): b:𝒯 𝒰(A)isContr( a:𝒯 𝒰(A)id 𝒯 𝒰(A)(a,b))\pi_2(\pi_2(\nabla(\mathrm{refl}_A))):\prod_{b:\mathcal{T}_\mathcal{U}(A)} \mathrm{isContr}\left(\sum_{a:\mathcal{T}_\mathcal{U}(A)} \mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(a, b)\right)

Definition in cubical type theory

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 judgmental version of identification elimination; only the typal 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 judgmental 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.

Categorical semantics

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 AA×AA\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 PAA×AP 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.

Prerequisites

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)(L,R). There are four obstacles in the way of such a construction.

  1. In order to handle the additional context Δ\Delta in the explicit definition above, it turns out to be necessary to assume that LL-maps are preserved by pullback along RR-maps between RR-objects. (Such a condition is also necessary in order to interpret type-theoretic dependent products in a locally cartesian closed category.)

  2. 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:YA(y):Typey\colon Y\vdash A(y)\colon Type is a dependent type and f:XYf\colon X\to Y is a morphism, then the identity type x:XId A(f(x))(,):Typex\colon X \vdash Id_{A(f(x))}(-,-)\colon Type is the same whether we first construct Id A(y)Id_{A(y)} and then substitute f(x)f(x) for yy, or first substitute f(x)f(x) for yy to obtain A(f(x))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.

  3. The eliminator term JJ 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.

  4. 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.

Interpretation in a type-theoretic model category

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 A:Type \vdash A : Type is as a fibrant object [A:Type][\vdash A : Type] which we will just write “AA” for short.

  • type formation

    The identity type a,b:AId A(a,b):Typea, b : A \vdash Id_A(a,b) : Type is interpreted as the path space object fibration

    A I A×A \array{ A^I \\ \downarrow \\ A \times A }
  • term introduction

    By definition of path space object, there exists a lift σ\sigma in

    A I σ A (id,id) A×A. \array{ && A^I \\ & {}^{\mathllap{\sigma}}\nearrow& \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    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):AA×A(id,id) : A \to A \times A.

    (id,id) *A I A I σ A = A (id,id) A×A. \array{ && (id,id)^* A^I &\to& A^I \\ &{}^{\mathllap{\sigma}}\nearrow& \downarrow & & \downarrow \\ A &=& A &\stackrel{(id,id)}{\to}& A \times A } \,.

    Since (id,id) *A I(id, id)^* A^I is the interpretation of the substitution
    a:AId A(a,a):Typea : A \vdash Id_A (a,a) : Type in this sense σ\sigma is now the interpretation of a term a:Ar A:Id A(a,a)a : A \vdash r_A : Id_A (a,a).

  • term elimination

    A type depending on an identity type

    a,b:A,p:Id A(a,b)C(a,b,p) a, b : A, p : Id_A(a,b) \vdash C(a,b,p)

    is interpreted as a fibration

    C A I. \array{ C \\ \downarrow \\ A^I } \,.

    The substitution C(a,a,r a)C(a,a,r_a) is interpreted by the pullback

    (id,id) *C C A (id,id) A×A. \array{ (id,id)^* C &\to& C \\ \downarrow && \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    Therefore a term t:C(a,a,r a)t : C(a,a,r_a) is interpreted as a section of this pullback

    (id,id) *C C t A = A (id,id) A×A. \array{ && (id,id)^* C &\to& C \\ &{}^{\mathllap{t}}\nearrow& \downarrow && \downarrow \\ A &=& A &\stackrel{(id,id)}{\to}& A \times A } \,.

    By the universal property of the pullback, this is equivalently a morphism tt in

    C t A (id,id) A×A. \array{ && C \\ & {}^{\mathllap{t}}\nearrow & \downarrow \\ A &\stackrel{(id,id)}{\to}& A \times A } \,.

    The elimination rule says that given such tt, there exists a compatible section of CA IC \to A^I. If we redraw the previous diagram as a square, then this section is a lift in that diagram

    A C r A I = A I. \array{ A &\to& C \\ {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow \\ A^I &=& A^I } \,.

    In particular, if CC itself is the pullback of a fibration DBD \to B along a morphism A IBA^I \to B, then rr has the left lifting property also against that fibration

    A C D r A I = A I B. \array{ A &\to& C &\to& D \\ {}^{\mathllap{r}}\downarrow &\nearrow& \downarrow && \downarrow \\ A^I &=& A^I &\to& B } \,.

    So the term elimination rule says that the interpretation AA IA \to A^I of a:Ar(a):Id A(a,a)a : A \vdash r(a) : Id_A (a,a) has the left lifting property against all fibrations, hence that AA IA \to A^I is to be interpreted as an acyclic cofibration.

Weak ω\omega-groupoids

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 LL-maps under pullback along RR-maps) seems to be necessary for the algebraic version of the result to go through.

References

The above Latin excerpts by Gottfried Leibniz are taken from

  • K. Gerhard (ed.), Section XIX, p. 228, 230 in: Die philosophischen Schriften von Gottfried Wilhelm Leibniz, Siebenter Band, Weidmannsche Buchhandlung (1890) [archive.org]

whose English translation is given in:

Explicit definition

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in

  • Per Martin-Löf, An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80, Elsevier (1975) 73-118 [doi:10.1016/S0049-237X(08)71945-1, CiteSeer]

and in the modern form of inference rules in

  • Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) [webpage, pdf, pdf]

with early survey in §1.0.1 of:

  • Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) [pdf, pdf]

For the two different ways of expressing the elimination and computation rules of identity types, see

See also (?):

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:

  • Lennard Götz, §4.2 of: Martin-Löf’s J-rule, LMU (2018) [pdf]

Discussion of issues of extensional/intensional type theory:

As inductive types

In (higher) observational type theory

Weak factorization systems

Types as \infty-groupoids

The suggestion that identity types witness groupoid and infinity-groupoid-structure is due to

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

Last revised on August 18, 2024 at 08:25:57. See the history of this page for a list of all contributions to it.