nLab two-type identity type



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





In dependent type theory, a version of the identity type where elements from two different types can be compared for equality. Given types AA and BB and an equivalence of types e:ABe:A \simeq B, the two-type identity type between two elements x:Ax:A and y:By:B is a type Id A,B(e,x,y)\mathrm{Id}_{A,B}(e, x, y) whose elements witness that xx and yy are “equal” over or modulo the equivalence ee.

The phrase “two-type identity type” is a placeholder name for a concept which may or may not have another name in the type theory literature. The idea however is that two-type identity types are the “non-dependent” versions of dependent identity types in that it directly compares elements between two equivalent types, rather than between a family of dependent types which are equivalent via transport across an identification in the index type.


Given types AA and BB, two-type identity types are an inductive family of types

e:AB,x:A,y:BId A,B(e,x,y)e:A \simeq B, x:A, y:B \vdash \mathrm{Id}_{A, B}(e, x, y)

generated by the family of elements

x:Atrefl A(x):Id A,A(id A,x,x)x:A \vdash \mathrm{trefl}_{A}(x):\mathrm{Id}_{A, A}(\mathrm{id}_A, x, x)

where id A\mathrm{id}_A is the identity equivalence on AA.

Inference rules

The inference rules for forming two-type identity types and terms are as follows. First the inference rule that defines the two-type identity type itself, as a dependent type, in some context Γ\Gamma.

Formation rule for two-type identity types:

ΓAtypeΓBtypeΓe:ABΓx:AΓy:BΓId A,B(e,a,b)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B \quad \Gamma \vdash x:A \quad \Gamma \vdash y:B}{\Gamma \vdash \mathrm{Id}_{A, B}(e, a, b) \; \mathrm{type}}

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

Introduction rule for two-type identity types:

ΓAtypeΓx:AΓtrefl A(x):Id A,A(id A,x,x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash x:A}{\Gamma \vdash \mathrm{trefl}_{A}(x):\mathrm{Id}_{A, A}(\mathrm{id}_A, x, x)}

Next we have the “elimination” rule:

Elimination rule for two-type identity types:

ΓAtypeΓBtype Γ,e:AB,x:A,y:B,q:Id A,B(e,x,y)C(e,x,y,q)type Γt: x:AC(Id A,x,x,trefl A,A(x)) Γe:ABΓx:AΓy:BΓq:Id A,B(e,x,y,q)Γind Id A,B(t,e,x,y,q):C(e,x,y,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, e:A \simeq B, x:A, y:B, q:\mathrm{Id}_{A, B}(e, x, y) \vdash C(e, x, y, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{x:A} C(\mathrm{Id}_A, x, x, \mathrm{trefl}_{A, A}(x)) \\ \Gamma \vdash e:A \simeq B \quad \Gamma \vdash x:A \quad \Gamma \vdash y:B \quad \Gamma \vdash q:\mathrm{Id}_{A, B}(e, x, y, q) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{Id}_{A, B}}(t, e, x, y, q):C(e, x, y, q)}

The elimination rule then says that if:

  1. for any equivalence e:ABe:A \simeq B, any elements x:Ax:A and y:By:B, and any two-type identification q:Id A,B(e,x,y)q:\mathrm{Id}_{A, B}(e, x, y) we have a type C(e,x,y,q)C(e, x, y, q), and
  2. we have a specified dependent function
    t: x:AC(id A,x,x,trefl A,A(x))t:\prod_{x:A} C(\mathrm{id}_A,x,x,\mathrm{trefl}_{A, A}(x))

then we can construct a canonically defined term called the eliminator

ind Id A,B(t,e,x,y,q):C(e,x,y,q)\mathrm{ind}_{\mathrm{Id}_{A, B}}(t,e,x,y,q):C(e,x,y,q)

for any ee, xx, yy, and qq.

Then, we have the computation rule or beta-reduction rule. This says that for all elements x:Ax:A, substituting the dependent function t: x:AC(id A,x,x,trefl A,A(x))t:\prod_{x:A} C(\mathrm{id}_A,x,x,\mathrm{trefl}_{A,A}(x)) into the eliminator along the constructor for xx yields an element equal to t(x)t(x) itself. Normally “equal” here means judgmental equality (a.k.a. definitional equality), but it is also possible for it to mean propositional equality (a.k.a. typal equality), so there are two possible computation rules

Computation rules for two-type identity types:

  • Judgmental computational rule

    ΓAtypeΓBtype Γ,e:AB,x:A,y:B,q:Id A,B(e,x,y)C(e,x,y,q)type Γt: x:AC(id A,x,x,trefl A,B(x))Γx:AΓind Id A,B(t,id A,x,x,trefl A,B(x))t(x):C(id A,x,x,trefl A,B(x))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, e:A \simeq B, x:A, y:B, q:\mathrm{Id}_{A, B}(e, x, y) \vdash C(e, x, y, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x)) \quad \Gamma \vdash x:A \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{Id}_{A, B}}(t, \mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x)) \equiv t(x):C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x))}
  • Propositional computational rule

    ΓAtypeΓBtype Γ,e:AB,x:A,y:B,q:Id A,B(e,x,y)C(e,x,y,q)type Γt: x:AC(id A,x,x,trefl A,B(x))Γx:AΓβ Id A,B(t,x):Id C(id A,x,x,trefl A,B(x))(ind Id A,B(t,id A,x,x,trefl A,B(x),t(x))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, e:A \simeq B, x:A, y:B, q:\mathrm{Id}_{A, B}(e, x, y) \vdash C(e, x, y, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x)) \quad \Gamma \vdash x:A \end{array} }{\Gamma \vdash \beta_{\mathrm{Id}_{A, B}}(t, x):\mathrm{Id}_{C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x))}(\mathrm{ind}_{\mathrm{Id}_{A, B}}(t, \mathrm{id}_A, x, x, \mathrm{trefl}_{A, B}(x), t(x))}

Finally, one might consider a uniqueness rule or eta-conversion rule. But similar to the case for identity types, a judgmental uniqueness rule for two-type identity types implies that the type theory is an extensional type theory, in which case there is not much need for two-type identity types, so such a rule is almost never written down. And as for identity types and other inductive types, the propositional/typal uniqueness rule is provable from the other four inference rules, so we don’t write it out explicitly.

Dependent universal property

The elimination, typal computation, and typal uniqueness rules for two-type identity types state that two-type identity types satisfy the dependent universal property of two-type identity types. With the uniqueness quantifier, the dependent universal property of two-type identity types could be simplified to the following rule:

ΓAtypeΓBtype Γ,e:AB,x:A,y:B,q:Id A,B(e,x,y)C(e,x,y,q)type Γt: x:AC(id A,x,x,trefl A(x))Γx:AΓup Id A,B(t,x):!J:( x:AC(id A,x,x,trefl A(x))) ( e:AB a:A b:B s:Id A,B(e,a,b)C(e,a,b,s)) .Id C(id A,x,x)(J(t,id A,x,x,trefl A(x)),t(x))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, e:A \simeq B, x:A, y:B, q:\mathrm{Id}_{A,B}(e, x, y) \vdash C(e, x, y, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x)) \quad \Gamma \vdash x:A \end{array} }{\Gamma \vdash \mathrm{up}_{\mathrm{Id}_{A, B}}(t, x): \begin{array}{c} \exists!J:\left(\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x))\right) \\ \to \left(\prod_{e:A \simeq B} \prod_{a:A} \prod_{b:B} \prod_{s:\mathrm{Id}_{A, B}(e, a, b)} C(e, a, b, s)\right) \\ .\mathrm{Id}_{C(\mathrm{id}_A, x, x)}(J(t, \mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x)), t(x)) \end{array} }

In natural language this states that given types AA and BB, and given a type family C(e,x,y,q)C(e, x, y, q) indexed by elements e:ABe:A \simeq B, x:Ax:A, y:By:B, and q:Id A,B(e,x,y)q:\mathrm{Id}_{A, B}(e, x, y), for all elements t: x:AC(id A,x,x,trefl A(x))t:\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x)) and x:Ax:A, there exists a unique function JJ with domain

x:AC(id A,x,x,trefl A(x))\prod_{x:A} C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x))

and codomain

e:AB a:A b:B s:Id A,B(e,a,b)C(e,a,b,s)\prod_{e:A \simeq B} \prod_{a:A} \prod_{b:B} \prod_{s:\mathrm{Id}_{A, B}(e, a, b)} C(e, a, b, s)

such that J(t,id A,x,x,trefl A(x))J(t, \mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x)) is equal to t(x)t(x) in the type C(id A,x,x,trefl A(x))C(\mathrm{id}_A, x, x, \mathrm{trefl}_{A}(x)).


Relation with identity types

One could then show that there exist equivalences between identity types and two-type identity types

Id A,B(e,x,y)Id B(e(x),y)\mathrm{Id}_{A, B}(e, x, y) \simeq \mathrm{Id}_{B}(e(x), y)


Id A,B(e,x,y)Id A(x,e 1(y))\mathrm{Id}_{A, B}(e, x, y) \simeq \mathrm{Id}_{A}(x, e^{-1}(y))

for all e:ABe:A \simeq B, x:Ax:A, and y:By:B.

Relation with dependent identity types

Dependent identity types hId x:A.B(x)(a,b,p,y,z)\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) are two-type identity type for which the equivalence used is transport transport x:A.B(x)(a,b,p):B(a)B(b)\mathrm{transport}_{x:A.B(x)}(a, b, p):B(a) \simeq B(b) across the given identification p:a= Abp:a =_A b:

hId x:A.B(x)(a,b,p,y,z)Id B(a),B(b)(transport x:A.B(x)(a,b,p),y,z)\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \coloneqq \mathrm{Id}_{B(a), B(b)}(\mathrm{transport}_{x:A.B(x)}(a, b, p), y, z)

On the other hand, every two-type identity type Id A,B(e,x,y)\mathrm{Id}_{A, B}(e, x, y) can be made into a dependent identity type. We first define a dependent type from the interval type x:𝕀C(x)x:\mathbb{I} \vdash C(x) defined as

  • C(left)AC(\mathrm{left}) \equiv A,

  • C(right)BC(\mathrm{right}) \equiv B, and

  • transport x:𝕀.C(x)(left,right,segment)e\mathrm{transport}_{x:\mathbb{I}.C(x)}(\mathrm{left}, \mathrm{right}, \mathrm{segment}) \equiv e


hId x:𝕀.C(x)(left,right,segment,x,y)Id A,B(e,y,z)\mathrm{hId}_{x:\mathbb{I}.C(x)}(\mathrm{left}, \mathrm{right}, \mathrm{segment}, x, y) \simeq \mathrm{Id}_{A, B}(e, y, z)


Given a Tarski universe (U,T)(U, T), there is an equivalence

Id T(A),T(B)(transport U(A,B,p),x,y)hId X:U.T(X)(A,B,p,x,y)\mathrm{Id}_{T(A), T(B)}(\mathrm{transport}_U(A, B, p), x, y) \simeq \mathrm{hId}_{X:U.T(X)}(A, B, p, x, y)

One could treat Russell universes as a Tarski universe whose type family is represented by the zero-width whitespace instead of TT, yielding

hId X:U.(X)(A,B,p,x,y)\mathrm{hId}_{X:U.(X)}(A, B, p, x, y)

for the dependent identity type and

Id A,B(idtoequiv U(A,B,p),x,y)hId X:U.(X)(A,B,p,x,y)\mathrm{Id}_{A, B}(\mathrm{idtoequiv}_U(A, B, p), x, y) \simeq \mathrm{hId}_{X:U.(X)}(A, B, p, x, y)

for the equivalence.

Given a Tarski universes (U,T)(U, T), if UU is univalent with equivalence

ua U(A,B):(A= UB)(T(A)T(B))\mathrm{ua}_U(A, B):(A =_U B) \simeq (T(A) \simeq T(B))

then there is an equivalence of types

Id T(A),T(B)(e,x,y)hId X:U.T(X)(A,B,ua U(A,B) 1(e),x,y)\mathrm{Id}_{T(A), T(B)}(e, x, y) \simeq \mathrm{hId}_{X:U.T(X)}(A, B, \mathrm{ua}_U(A, B)^{-1}(e), x, y)

for UU-small types A:UA:U and B:UB:U and equivalence e:ABe:A \simeq B

For Russell universes UU, the univalence axiom is represented by

ua U(A,B):(A= UB)(AB)\mathrm{ua}_U(A, B):(A =_U B) \simeq (A \simeq B)

and the above equivalence is represented by

Id A,B(e,x,y)hId A,B(ua U(A,B) 1(e),x,y)\mathrm{Id}_{A, B}(e, x, y) \simeq \mathrm{hId}_{A, B}(\mathrm{ua}_U(A, B)^{-1}(e), x, y)

for the equivalence.

One-to-one correspondence structure

Two-type identity types are one-to-one correspondences. Given an equivalence e:ABe:A \simeq B,

  • for all elements y:By:B, there exists a unique element x:Ax:A such that Id A,B(e,x,y)\mathrm{Id}_{A, B}(e, x, y); the witness is given by the right projection function of the equivalence e:ABe:A \simeq B
π 2(e): y:B!x:A.Id A,B(e,x,y)\pi_2(e):\prod_{y:B} \exists!x:A.\mathrm{Id}_{A, B}(e, x, y)
  • for all elements x:Ax:A, there exists a unique element y:By:B such that Id A,B(e,x,y)\mathrm{Id}_{A, B}(e, x, y); the witness is given by the right projection function of the inverse equivalence e 1:BAe^{-1}:B \simeq A
π 2(e 1): x:A!y:B.Id A,B(e,x,y)\pi_2(e^{-1}):\prod_{x:A} \exists!y:B.\mathrm{Id}_{A, B}(e, x, y)

Last revised on September 17, 2023 at 11:11:36. See the history of this page for a list of all contributions to it.