nLab heterogeneous identity type

Redirected from "dependent identity types".
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 dependent type theory, a heterogeneous identity type or dependent identity type is a version of the identity type where given a type AA, a type family x:AB(x)x:A \vdash B(x), terms a:Aa:A, b:Ab:A, and an identification p:a= Abp:a =_A b, the heterogeneous identity type between two elements y:B(a)y:B(a) and z:B(b)z:B(b) is a type whose elements witness that yy and zz are “equal” over or modulo the identification pp.

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
heterogeneous identity typeheterogeneous identities
heterogeneous path typeheterogeneous paths
heterogeneous identification typeheterogeneous identifications
heterogeneous equality typeheterogeneous equalities

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

  • The name “heterogeneous identity type” comes from the fact that the dependent identity type is the canonical one-to-one correspondence x:B(a),y:B(b)Id B p(x,y)x:B(a), y:B(b) \vdash \mathrm{Id}_B^p(x, y) of the transport equivalence tr B p:B(a)B(b)\mathrm{tr}_B^p:B(a) \simeq B(b) on a type family x:AB(x)x:A \vdash B(x) and an identification p:a= Abp:a =_A b, which is the dependent/heterogeneous version of the identity type for the identity equivalence id A:AA\mathrm{id}_A:A \simeq A

  • The name “heterogeneous path type” comes from the fact that, in a context where terms of ordinary identity types can be represented as functions from an interval type, the terms of the heterogeneous identity type can similarly be represented as dependent functions from the interval type. For instance, this is true in some categorical semantics and in cubical type theory.

Definitions

Using identity types

There are many different ways to define heterogeneous identity types. The simplest definition states that given a type family x:AB(x)x:A \vdash B(x), heterogeneous identity types are an inductive family of types

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

generated by the family of elements called “heterogeneous reflexivity”

a:A,y:B(a)hrefl x:A.B(x)(a,y):hId x:A.B(x)(a,a,refl A(a),y,y)a:A, y:B(a) \vdash \mathrm{hrefl}_{x:A.B(x)}(a, y):\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)

Inference rules

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

Formation rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γa:AΓb:AΓp:Id A(a,b)Γy:B(a)Γz:B(b)ΓhId x:A.B(x)(a,b,p,y,z)type\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \end{array} }{\Gamma \vdash \mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \; \mathrm{type}}

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

Introduction rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γa:AΓy:B(a)Γhrefl x:A.B(x)(a,y):hId x:A.B(x)(a,a,refl A(a),y,y)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \mathrm{hrefl}_{x:A.B(x)}(a, y):\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)}

Next we have the “elimination” rule:

Elimination rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:Id A(a,b),y:B(a),z:B(b),q:hId x:A.B(x)(a,b,p,y,z)C(a,b,p,y,z,q)type Γt: a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y)) Γa:AΓb:AΓp:Id A(a,b)Γy:B(a)Γz:B(b)Γq:hId x:A.B(x)(a,b,p,y,z)Γind hId x:A.B(x)(t,a,b,p,y,z,q):C(a,b,p,y,z,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B(a) \quad \Gamma \vdash z:B(b) \quad \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, y, z, q):C(a, b, p, y, z, q)}

The elimination rule then says that if:

  1. for any elements a:Aa:A and b:Ab:A, any identification p:Id A(a,b)p:\mathrm{Id}_A(a,b), any elements y:B(a)y:B(a) and z:B(b)z:B(b), and any heterogeneous identification q:hId x:A.B(x)(a,b,p,y,z)q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) we have a type C(a,b,p,y,z,q)C(a, b, p, y, z, q), and
  2. we have a specified dependent function
    t: a:A y:B(a)C(a,a,refl A(x),y,y,hrefl x:A.B(x)(a,y))t:\prod_{a:A} \prod_{y:B(a)} C(a,a,\mathrm{refl}_A(x),y,y,\mathrm{hrefl}_{x:A.B(x)}(a, y))

then we can construct a canonically defined term called the eliminator

ind hId x:A.B(x)(t,a,b,p,y,z,q):C(a,b,p,y,z,q)\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t,a,b,p,y,z,q):C(a,b,p,y,z,q)

for any aa, bb, pp, yy, zz, and qq.

Then, we have the computation rule or beta-reduction rule. This says that for all elements a:Aa:A and y:B(a)y:B(a), substituting the dependent function t: a:A y:B(a)C(a,a,refl A(x),y,y,hrefl x:A.B(x)(a,y))t:\prod_{a:A} \prod_{y:B(a)} C(a,a,\mathrm{refl}_A(x),y,y,\mathrm{hrefl}_{x:A.B(x)}(a, y)) into the eliminator along heterogeneous reflexivity for aa and yy yields an element equal to t(a,y)t(a, y) 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 heterogeneous identity types:

  • Judgmental computational rule

    ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:Id A(a,b),y:B(a),z:B(b),q:hId x:A.B(x)(a,b,p,y,z)C(a,b,p,y,z,q)type Γt: a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))Γa:AΓy:B(a)Γind hId x:A.B(x)(t,a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))t(a,y):C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \quad \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \equiv t(a, y):C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))}
  • Propositional computational rule

    ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:Id A(a,b),y:B(a),z:B(b),q:hId x:A.B(x)(a,b,p,y,z)C(a,b,p,y,z,q)type Γt: a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))Γa:AΓy:B(a)Γβ hId x:A.B(x)(t,a,y):Id C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))(ind hId x:A.B(x)(t,a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y),t(a,y))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \quad \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \beta_{\mathrm{hId}_{x:A.B(x)}}(t, a, y):\mathrm{Id}_{C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))}(\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y), t(a, y))}

Finally, one might consider a uniqueness rule or eta-conversion rule. But similar to the case for identity types, a judgmental uniqueness rule for heterogeneous identity types implies that the type theory is an extensional type theory, in which case there is not much need for heterogeneous 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 heterogeneous identity types state that heterogeneous identity types satisfy the dependent universal property of heterogeneous identity types. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of heterogeneous identity types could be simplified to the following rule:

ΓAtypeΓ,x:AB(x)type Γ,a:A,b:A,p:Id A(a,b),y:B(a),z:B(b),q:hId x:A.B(x)(a,b,p,y,z)C(a,b,p,y,z,q)type Γt: a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y)) Γa:AΓy:B(a)Γup hId x:A.B(x)(t,f,a,b,p):!J:( a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))) ( c:A d:A r:Id A(c,d) e:B(c) f:B(c) s:hId x:A.B(x)(c,d,r,e,f)C(c,d,r,e,f,s)) .Id C(a,a,refl A(a),y,y)(J(t,a,a,refl A,y,y,hrefl x:A.B(x)(a,y)),t(a,y))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \\ \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \mathrm{up}_{\mathrm{hId}_{x:A.B(x)}}(t, f, a, b, p): \begin{array}{c} \exists!J:\left(\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))\right) \\ \to \left(\prod_{c:A} \prod_{d:A} \prod_{r:\mathrm{Id}_A(c, d)} \prod_{e:B(c)} \prod_{f:B(c)} \prod_{s:\mathrm{hId}_{x:A.B(x)}(c, d, r, e, f)} C(c, d, r, e, f, s)\right) \\ .\mathrm{Id}_{C(a, a, \mathrm{refl}_A(a), y, y)}(J(t, a, a, \mathrm{refl}_A, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)), t(a, y)) \end{array} }

In natural language this states that given a type AA, a type family B(x)B(x) indexed by elements x:Ax:A, and given a type family C(a,b,p,y,z,q)C(a, b, p, y, z, q) indexed by elements a:Aa:A, b:Ab:A, p:Id A(a,b)p:\mathrm{Id}_A(a, b), y:B(a)y:B(a), z:B(b)z:B(b), and q:hId x:A.B(x)(a,b,p,y,z)q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), for all elements t: a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))t:\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)), a:Aa:A, and y:B(a)y:B(a), there exists a unique function JJ with domain

a:A y:B(a)C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))\prod_{a:A} \prod_{y:B(a)} C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))

and codomain

c:A d:A r:Id A(c,d) e:B(c) f:B(c) s:hId x:A.B(x)(c,d,r,e,f)C(c,d,r,e,f,s)\prod_{c:A} \prod_{d:A} \prod_{r:\mathrm{Id}_A(c, d)} \prod_{e:B(c)} \prod_{f:B(c)} \prod_{s:\mathrm{hId}_{x:A.B(x)}(c, d, r, e, f)} C(c, d, r, e, f, s)

such that J(t,a,a,refl A,y,y,hrefl x:A.B(x)(a,y))J(t, a, a, \mathrm{refl}_A, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) is equal to t(a,y)t(a, y) in the type C(a,a,refl A(a),y,y,hrefl x:A.B(x)(a,y))C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)).

Using function types from the interval type

There is another notion of heterogeneous identity type, which uses functions from the interval type f:𝕀Af:\mathbb{I} \to A, rather than elements a:Aa:A, b:Ab:A, and p:a= Abp:a =_A b:

Given a type family x:AB(x)x:A \vdash B(x), heterogeneous identity types are an inductive family of types

f:𝕀A,y:B(f(0)),z:B(f(1))hId x:A.B(x)(f,y,z)f:\mathbb{I} \to A, y:B(f(0)), z:B(f(1)) \vdash \mathrm{hId}_{x:A.B(x)}(f, y, z)

generated by the family of elements called “heterogeneous reflexivity”

a:A,y:B(a)hrefl x:A.B(x)(a,y):hId x:A.B(x)(λi:𝕀.a,y,y)a:A, y:B(a) \vdash \mathrm{hrefl}_{x:A.B(x)}(a, y):\mathrm{hId}_{x:A.B(x)}(\lambda i:\mathbb{I}.a, y, y)

since by definition of constant function we have that

(λi:𝕀.a)(0)a(λi:𝕀.a)(1)a(\lambda i:\mathbb{I}.a)(0) \equiv a \qquad (\lambda i:\mathbb{I}.a)(1) \equiv a

Inference rules

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

Formation rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γf:𝕀AΓy:B(f(0))Γz:B(f(1))ΓhId x:A.B(x)(f,y,z)type\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash f:\mathbb{I} \to A \quad \Gamma \vdash y:B(f(0)) \quad \Gamma \vdash z:B(f(1)) \end{array} }{\Gamma \vdash \mathrm{hId}_{x:A.B(x)}(f, y, z) \; \mathrm{type}}

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

Introduction rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γa:AΓy:B(a)Γhrefl x:A.B(x)(a,y):hId x:A.B(x)(λi:𝕀.a,y,y)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \mathrm{hrefl}_{x:A.B(x)}(a, y):\mathrm{hId}_{x:A.B(x)}(\lambda i:\mathbb{I}.a, y, y)}

Next we have the “elimination” rule:

Elimination rule for heterogeneous identity types:

ΓAtypeΓ,x:AB(x)type Γ,f:𝕀A,y:B(f(0)),z:B(f(1)),q:hId x:A.B(x)(f,y,z)C(f,y,z,q)type Γt: a:A y:B(a)C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y)) Γf:𝕀AΓy:B(f(0))Γz:B(f(1))Γq:hId x:A.B(x)(f,y,z)Γind hId x:A.B(x)(t,f,y,z,q):C(f,y,z,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, f:\mathbb{I} \to A, y:B(f(0)), z:B(f(1)), q:\mathrm{hId}_{x:A.B(x)}(f, y, z) \vdash C(f, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(\lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \\ \Gamma \vdash f:\mathbb{I} \to A \quad \Gamma \vdash y:B(f(0)) \quad \Gamma \vdash z:B(f(1)) \quad \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(f, y, z) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, f, y, z, q):C(f, y, z, q)}

The elimination rule then says that if:

  1. for any function f:𝕀Af:\mathbb{I} \to A, any elements y:B(f(0))y:B(f(0)) and z:B(f(1))z:B(f(1)), and any heterogeneous identification q:hId x:A.B(x)(f,y,z)q:\mathrm{hId}_{x:A.B(x)}(f, y, z) we have a type C(f,y,z,q)C(f, y, z, q), and
  2. we have a specified dependent function
    t: a:A y:B(a)C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))t:\prod_{a:A} \prod_{y:B(a)} C(\lambda i:\mathbb{I}.a,y,y,\mathrm{hrefl}_{x:A.B(x)}(a, y))

then we can construct a canonically defined term called the eliminator

ind hId x:A.B(x)(t,f,y,z,q):C(a,b,p,y,z,q)\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t,f,y,z,q):C(a,b,p,y,z,q)

for any ff, yy, zz, and qq.

Then, we have the computation rule or beta-reduction rule. This says that for all elements a:Aa:A and y:B(a)y:B(a), substituting the dependent function t: a:A y:B(a)C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))t:\prod_{a:A} \prod_{y:B(a)} C(\lambda i:\mathbb{I}.a,y,y,\mathrm{hrefl}_{x:A.B(x)}(a, y)) into the eliminator along heterogeneous reflexivity for aa and yy yields an element equal to t(a,y)t(a, y) 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 heterogeneous identity types:

  • Judgmental computational rule

    ΓAtypeΓ,x:AB(x)type Γ,f:𝕀A,y:B(f(0)),z:B(f(1)),q:hId x:A.B(x)(f,y,z)C(f,y,z,q)type Γt: a:A y:B(a)C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))Γa:AΓy:B(a)Γind hId x:A.B(x)(t,λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))t(a,y):C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, f:\mathbb{I} \to A, y:B(f(0)), z:B(f(1)), q:\mathrm{hId}_{x:A.B(x)}(f, y, z) \vdash C(f, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(\lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \quad \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, \lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \equiv t(a, y):C(\lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))}
  • Propositional computational rule

    ΓAtypeΓ,x:AB(x)type Γ,f:𝕀A,y:B(f(0)),z:B(f(1)),q:hId x:A.B(x)(f,y,z)C(f,y,z,q)type Γt: a:A y:B(a)C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))Γa:AΓy:B(a)Γβ hId x:A.B(x)(t,a,y):Id C(λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y))(ind hId x:A.B(x)(t,λi:𝕀.a,y,y,hrefl x:A.B(x)(a,y),t(a,y))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, f:\mathbb{I} \to A, y:B(f(0)), z:B(f(1)), q:\mathrm{hId}_{x:A.B(x)}(f, y, z) \vdash C(f, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{a:A} \prod_{y:B(a)} C(\lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y)) \quad \Gamma \vdash a:A \quad \Gamma \vdash y:B(a) \end{array} }{\Gamma \vdash \beta_{\mathrm{hId}_{x:A.B(x)}}(t, a, y):\mathrm{Id}_{C(\lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))}(\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, \lambda i:\mathbb{I}.a, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y), t(a, y))}

Finally, one might consider a uniqueness rule or eta-conversion rule. But similar to the case for identity types, a judgmental uniqueness rule for heterogeneous identity types implies that the type theory is an extensional type theory, in which case there is not much need for heterogeneous 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.

From two-type identity types

Given two-type identity types in the type theory, heterogeneous identity types between y:B(a)y:B(a) and z:B(b)z:B(b) across the path p:a= Abp:a =_A b could be defined as the two-type identity type between y:B(a)y:B(a) and z:B(b)z:B(b) across the transport equivalence transport x:A.B(x)(a,b,p)\mathrm{transport}_{x:A.B(x)}(a, b, p)

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)

Properties

Groupoidal structure of heterogeneous identity types

Reflexivity of heterogeneous identifications is already given in the introduction rule of heterogeneous identity types.

Definition

Given

  • a type family x:AB(x)x:A \vdash B(x),

  • elements a 1:Aa_1:A, a 2:Aa_2:A, a 3:Aa_3:A,

  • identifications p 1:Id A(a 1,a 2)p_1:\mathrm{Id}_A(a_1, a_2) and p 2:Id A(a 2,a 3)p_2:\mathrm{Id}_A(a_2, a_3),

  • elements y 1:B(a 1)y_1:B(a_1), y 2:B(a 2)y_2:B(a_2), and y 3:B(a 3)y_3:B(a_3),

there is a function called the concatenation of heterogeneous identifications

()():hId x:A.B(x)(a 1,a 2,p 1,y 1,y 2)×hId x:A.B(x)(a 2,a 3,p 2,y 2,y 3)hId x:A.B(x)(a 1,a 3,p 1p 2,y 1,y 3)(-) \bullet (-):\mathrm{hId}_{x:A.B(x)}(a_1, a_2, p_1, y_1, y_2) \times \mathrm{hId}_{x:A.B(x)}(a_2, a_3, p_2, y_2, y_3) \to \mathrm{hId}_{x:A.B(x)}(a_1, a_3, p_1 \bullet p_2, y_1, y_3)

defined by double induction on heterogeneous reflexivity for a:Aa:A and y:B(a)y:B(a)

hrefl A(a,y)hrefl A(a,y)hrefl A(a,y)\mathrm{hrefl}_A(a, y) \bullet \mathrm{hrefl}_A(a, y) \equiv \mathrm{hrefl}_A(a, y)

in the type

hId x:A.B(x)(a,a,refl A(a),y,y)\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)

Definition

Given

  • a type family x:AB(x)x:A \vdash B(x),

  • elements a:Aa:A, b:Ab:A

  • identifications p:Id A(a,b)p:\mathrm{Id}_A(a, b)

  • elements y:B(a)y:B(a), z:B(b)z:B(b),

there is a dependent function called the left unitor of heterogeneous identifications

hlunitor: q:hId x:A.B(x)(a,b,p,y,z)Id hId x:A.B(x)(a,b,p,y,z)(hrefl A(a,y)q,q)\mathrm{hlunitor}:\prod_{q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)} \mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)}(\mathrm{hrefl}_A(a, y) \bullet q, q)

defined by induction on heterogeneous reflexivity for a:Aa:A and y:B(a)y:B(a):

hlunitor(hrefl A(a,y))refl hId x:A.B(x)(a,a,refl A(a),y,y)(hrefl A(a,y))\mathrm{hlunitor}(\mathrm{hrefl}_A(a, y)) \equiv \mathrm{refl}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)}(\mathrm{hrefl}_A(a, y))

in the type

Id hId x:A.B(x)(a,a,refl A(a),y,y)(hrefl A(a,y)hrefl A(a,y),hrefl A(a,y))\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)}(\mathrm{hrefl}_A(a, y) \bullet \mathrm{hrefl}_A(a, y), \mathrm{hrefl}_A(a, y))

Definition

Given

  • a type family x:AB(x)x:A \vdash B(x),

  • elements a:Aa:A, b:Ab:A

  • identifications p:Id A(a,b)p:\mathrm{Id}_A(a, b)

  • elements y:B(a)y:B(a), z:B(b)z:B(b),

there is a dependent function called the right unitor of heterogeneous identifications

hrunitor: q:hId x:A.B(x)(a,b,p,y,z)Id hId x:A.B(x)(a,b,p,y,z)(qhrefl A(b,z),q)\mathrm{hrunitor}:\prod_{q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)} \mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)}(q \bullet \mathrm{hrefl}_A(b, z), q)

defined by induction on heterogeneous reflexivity for b:Bb:B and z:B(b)z:B(b)

hrunitor(hrefl A(b,z))refl hId x:A.B(x)(b,b,refl A(b),z,z)(hrefl A(b,z))\mathrm{hrunitor}(\mathrm{hrefl}_A(b, z)) \equiv \mathrm{refl}_{\mathrm{hId}_{x:A.B(x)}(b, b, \mathrm{refl}_A(b), z, z)}(\mathrm{hrefl}_A(b, z))

in the type

Id hId x:A.B(x)(b,b,refl A(b),z,z)(hrefl A(b,z)hrefl A(b,z),hrefl A(b,z))\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(b, b, \mathrm{refl}_A(b), z, z)}(\mathrm{hrefl}_A(b, z) \bullet \mathrm{hrefl}_A(b, z), \mathrm{hrefl}_A(b, z))

Definition

Given

  • a type family x:AB(x)x:A \vdash B(x),

  • elements a 1:Aa_1:A, a 2:Aa_2:A, a 3:Aa_3:A, a 4:Aa_4:A

  • identifications p 1:Id A(a 1,a 2)p_1:\mathrm{Id}_A(a_1, a_2), p 2:Id A(a 2,a 3)p_2:\mathrm{Id}_A(a_2, a_3), p 3:Id A(a 3,a 4)p_3:\mathrm{Id}_A(a_3, a_4),

  • elements y 1:B(a 1)y_1:B(a_1), y 2:B(a 2)y_2:B(a_2), y 3:B(a 3)y_3:B(a_3), y 4:B(a 4)y_4:B(a_4),

there is a dependent function called the associator of heterogeneous identifications

hassoc: q 1:hId x:A.B(x)(a 1,a 2,p 1,y 1,y 2) q 2:hId x:A.B(x)(a 2,a 3,p 2,y 2,y 3) q 3:hId x:A.B(x)(a 3,a 4,p 3,y 3,y 4)Id hId x:A.B(x)(a 1,a 4,assoc(p 1,p 2,p 3),y 1,y 4)(q 1(q 2q 3),(q 1q 2)q 3)\mathrm{hassoc}:\prod_{q_1:\mathrm{hId}_{x:A.B(x)}(a_1, a_2, p_1, y_1, y_2)} \prod_{q_2:\mathrm{hId}_{x:A.B(x)}(a_2, a_3, p_2, y_2, y_3)} \prod_{q_3:\mathrm{hId}_{x:A.B(x)}(a_3, a_4, p_3, y_3, y_4)} \mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a_1, a_4, \mathrm{assoc}(p_1, p_2, p_3), y_1, y_4)}(q_1 \bullet (q_2 \bullet q_3), (q_1 \bullet q_2) \bullet q_3)

defined by triple induction on heterogeneous reflexivity for a:Aa:A and y:B(a)y:B(a)

hassoc(hrefl A(a,y),hrefl A(a,y),hrefl A(a,y))refl hId x:A.B(x)(a,a,refl A(a),y,y)(hrefl A(a,y))\mathrm{hassoc}(\mathrm{hrefl}_A(a, y), \mathrm{hrefl}_A(a, y), \mathrm{hrefl}_A(a, y)) \equiv \mathrm{refl}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)}(\mathrm{hrefl}_A(a, y))

in the type

Id hId x:A.B(x)(a,a,refl A(a),y,y)(hrefl A(a,y)(hrefl A(a,y)hrefl A(a,y)),(hrefl A(a,y)hrefl A(a,y))hrefl A(a,y))\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)}(\mathrm{hrefl}_A(a, y) \bullet (\mathrm{hrefl}_A(a, y) \bullet \mathrm{hrefl}_A(a, y)), (\mathrm{hrefl}_A(a, y) \bullet \mathrm{hrefl}_A(a, y)) \bullet \mathrm{hrefl}_A(a, y))

Definition

Given

  • a type family x:AB(x)x:A \vdash B(x),

  • elements a 1:Aa_1:A, a 2:Aa_2:A

  • identifications p 1:Id A(a 1,a 2)p_1:\mathrm{Id}_A(a_1, a_2)

  • elements y 1:B(a 1)y_1:B(a_1), y 2:B(a 2)y_2:B(a_2),

there is a function called the inverse of heterogeneous identifications

inv(a 1,a 2,p 1,y 1,y 2):hId x:A.B(x)(a 1,a 2,p 1,y 1,y 2)hId x:A.B(x)(a 2,a 1,p 1 1,y 2,y 1)\mathrm{inv}(a_1, a_2, p_1, y_1, y_2):\mathrm{hId}_{x:A.B(x)}(a_1, a_2, p_1, y_1, y_2) \to \mathrm{hId}_{x:A.B(x)}(a_2, a_1, p_1^{-1}, y_2, y_1)

defined by induction on heterogeneous reflexivity:

a:A,y:B(a)inv(a,a,refl A(a),y,y)(hrefl A(a,y))hrefl A(a,y):hId x:A.B(x)(a,a,refl A(a),y,y)hId x:A.B(x)(a,a,refl A(a),y,y)a:A, y:B(a) \vdash \mathrm{inv}(a, a, \mathrm{refl}_A(a), y, y)(\mathrm{hrefl}_A(a, y)) \equiv \mathrm{hrefl}_A(a, y):\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y) \to \mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)

Relation between identity types and heterogeneous identity types

There are equivalences between identity types and heterogeneous identity types

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

and

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

for all a:Aa:A, b:Ab:A, p:Id A(a,b)p:\mathrm{Id}_A(a, b), y:B(a)y:B(a), and z:B(b)z:B(b). For constant families x:ABx:A \vdash B, transport x:A.B(a,b,p)(y)y\mathrm{transport}_{x:A.B}(a, b, p)(y) \coloneqq y and transport x:A.B(a,b,p) 1(z)z\mathrm{transport}_{x:A.B}(a, b, p)^{-1}(z) \coloneqq z, so the above two equivalences simplify down to

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

for constant type families x:ABx:A \vdash B.

One-to-one correspondence structure

Heterogeneous identity types are one-to-one correspondences. Given elements a:Aa:A, b:Ab:A, and p:Id A(a,b)p:\mathrm{Id}_A(a, b),

  • for all elements z:B(b)z:B(b), there exists a unique element y:B(a)y:B(a) such that hId x:A.B(x)(a,b,p,y,z)\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z); the witness is given by the right projection function of transport across pp, 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)
π 2(transport x:A.B(x)(a,b,p)): z:B(b)!y:B(a).hId x:A.B(x)(a,b,p,y,z)\pi_2(\mathrm{transport}_{x:A.B(x)}(a, b, p)):\prod_{z:B(b)} \exists!y:B(a).\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)
  • for all elements y:B(a)y:B(a), there exists a unique element z:B(b)z:B(b) such that hId x:A.B(x)(a,b,p,y,z)\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z); the witness is given by the right projection function of the inverse transport across pp, transport x:A.B(x)(a,b,p) 1:B(b)B(a)\mathrm{transport}_{x:A.B(x)}(a, b, p)^{-1}:B(b) \simeq B(a)
π 2(transport x:A.B(x)(a,b,p) 1): y:B(a)!z:B(b).hId x:A.B(x)(a,b,p,y,z)\pi_2(\mathrm{transport}_{x:A.B(x)}(a, b, p)^{-1}):\prod_{y:B(a)} \exists!z:B(b).\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)

Function application to identifications

The dependent function application to identifications is defined in the usual way, by induction on the identity type of the index type:

  • given a type AA, a type family x:AB(x)x:A \vdash B(x), and a dependent function f: x:AB(x)f:\prod_{x:A} B(x), there are dependent functions
apd x:A.B(x)(f): a:A b:A p:Id A(a,b)hId x:A.B(x)(a,b,p,f(a),f(b))\mathrm{apd}_{x:A.B(x)}(f):\prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} \mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b))

inductively defined respectively by:

apd x:A.B(x)(f,a,a,refl A(a))hrefl x:A.B(x)(a,a,refl A(a),f(a),f(a)):hId x:A.B(x)(a,a,refl A(a),f(a),f(a))\mathrm{apd}_{x:A.B(x)}(f, a, a, \mathrm{refl}_A(a)) \equiv \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), f(a), f(a)):\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), f(a), f(a))

Extensionality principles

Heterogeneous identity types are used in many extensionality principles.

ext : f:AB g:ABId AB(f,g) a:A b:A p:Id A(a,b)hId B(a,b,p,f(a),g(b))\mathrm{ext}_{\to}:\prod_{f:A \to B} \prod_{g:A \to B} \mathrm{Id}_{A \to B}(f, g) \simeq \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} \mathrm{hId}_{B}(a, b, p, f(a), g(b))
ext Π: f: x:AB(x) g: x:AB(x)Id x:AB(x)(f,g) a:A b:A p:Id A(a,b)hId x:A.B(x)(a,b,p,f(a),g(b))\mathrm{ext}_\Pi:\prod_{f:\prod_{x:A} B(x)} \prod_{g:\prod_{x:A} B(x)} \mathrm{Id}_{\prod_{x:A} B(x)}(f, g) \simeq \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} \mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), g(b))
  • The extensionality principle for product types states that there is an equivalence
ext ×: s:A×B t:A×BId A×B(s,t) p:Id A(π 1(s),π 1(t))hId B(π 1(s),π 1(t),p,π 2(s),π 2(t))\mathrm{ext}_{\times}:\prod_{s:A \times B} \prod_{t:A \times B} \mathrm{Id}_{A \times B}(s, t) \simeq \sum_{p:\mathrm{Id}_A(\pi_1(s), \pi_1(t))} \mathrm{hId}_{B}(\pi_1(s), \pi_1(t), p, \pi_2(s), \pi_2(t))
ext Σ: s: x:AB(x) t: x:AB(x)Id x:AB(x)(s,t) p:Id A(π 1(s),π 1(t))hId x:A.B(x)(π 1(s),π 1(t),p,π 2(s),π 2(t))\mathrm{ext}_\Sigma:\prod_{s:\sum_{x:A} B(x)} \prod_{t:\sum_{x:A} B(x)} \mathrm{Id}_{\sum_{x:A} B(x)}(s, t) \simeq \sum_{p:\mathrm{Id}_A(\pi_1(s), \pi_1(t))} \mathrm{hId}_{x:A.B(x)}(\pi_1(s), \pi_1(t), p, \pi_2(s), \pi_2(t))

Inference rules for higher inductive types

Whenever there is an identification given in an introduction rule for a higher inductive type, one of the hypothesis in the elimination and computation rules for the higher inductive types is a judgment of a term of the corresponding heterogeneous identification type along the given identification in the introduction rule.

For example, the introduction rules for the circle type S 1S^1 state that one could construct an element 𝒷:S 1\mathcal{b}:S^1 and an identification 𝓁:Id S 1(𝒷,𝒷)\mathcal{l}:\mathrm{Id}_{S^1}(\mathcal{b}, \mathcal{b}). The elimination rule for the circle type states that given the hypotheses of

  • a type family x:S 1C(x)x:S^1 \vdash C(x),

  • an element c 𝒷:C(𝒷)c_\mathcal{b}:C(\mathcal{b}),

  • a heterogeneous identification c 𝓁:hId x:S 1.C(x)(𝒷,𝒷,𝓁,c 𝒷,c 𝒷)c_\mathcal{l}:\mathrm{hId}_{x:S^1.C(x)}(\mathcal{b}, \mathcal{b}, \mathcal{l}, c_\mathcal{b}, c_\mathcal{b}),

one could construct the family of elements p:S 1ind S 1(c 𝒷,c 𝓁)(p):C(p)p:S^1 \vdash \mathrm{ind}_{S^1}(c_\mathcal{b}, c_\mathcal{l})(p):C(p).

Categorical semantics

needs to be written

In cubical type theory

The path types in cubical type theory are heterogeneous path types. See cubical path type for more details.

In higher observational type theory

In higher observational type theory, the heterogeneous identity type is a primitive type former (although depending on the presentation, it can also be obtained using apap into the universe). In its general form, the type family can depend not just on a single type but on a type telescope Δ\Delta. The resulting heterogeneous identity type then depends on an “identification in that telescope”, which is defined by mutual recursion as a telescope of heterogeneous identity types. The formation rule is then

ς:δ= Δδ δAtypea:A[δ]a :A[δ ]a= Δ.A ςa type\frac{\varsigma:\delta =_\Delta \delta^{'} \quad \delta \vdash A\; \mathrm{type} \quad a:A[\delta] \quad a^{'}:A[\delta^{'}]}{a =_{\Delta.A}^\varsigma a^{'}\; \mathrm{type}}

… needs to be finished

Heterogeneous identity types in universes

Given a term of a universe A:𝒰A:\mathcal{U}, a judgment z:𝒯 𝒰(A)B:𝒰z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U}, terms x:𝒯 𝒰(A)x:\mathcal{T}_\mathcal{U}(A) and y:𝒯 𝒰(A)y:\mathcal{T}_\mathcal{U}(A), and an identity p:id 𝒯 𝒰(A)(x,y)p:\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(x,y), we have

ap z.B(p):id 𝒰(B(x),B(y))\mathrm{ap}_{z.B}(p):\mathrm{id}_\mathcal{U}(B(x),B(y))

and

(u,v):𝒯 𝒰(B(x))×𝒯 𝒰(B(y))π 1((ap z.B(p)))(u,v):𝒰(u,v):\mathcal{T}_\mathcal{U}(B(x)) \times \mathcal{T}_\mathcal{U}(B(y)) \vdash \pi_1(\nabla(\mathrm{ap}_{z.B}(p)))(u,v):\mathcal{U}

We could define a heterogeneous identity type as

id 𝒯 𝒰(z.B) p(u,v)π 1((ap z.B(p)))(u,v)\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{p}(u, v) \coloneqq \pi_1(\nabla(\mathrm{ap}_{z.B}(p)))(u, v)

There is a rule

A:𝒰z:𝒯 𝒰(A)B:𝒰a:𝒯 𝒰(A)id 𝒯 𝒰(z.B) refl a(u,v)id 𝒯 𝒰(B[a/z])(u,v)\frac{A:\mathcal{U} \quad z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U} \quad a:\mathcal{T}_\mathcal{U}(A)}{\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{\refl_{a}}(u, v) \equiv \mathrm{id}_{\mathcal{T}_\mathcal{U}(B[a/z])}(u, v)}

and for constant families B:𝒰B:\mathcal{U}

id 𝒯 𝒰(z.B) p(u,v)id 𝒯 𝒰(B)(u,v)\mathrm{id}_{\mathcal{T}_\mathcal{U}(z.B)}^{p}(u, v) \equiv \mathrm{id}_{\mathcal{T}_\mathcal{U}(B)}(u, v)

A variant using dependent function types

There is a variant of heterogeneous identity types which uses a dependent function f: x:AB(x)f:\prod_{x:A} B(x) instead of two elements y:B(a)y:B(a) and z:B(b)z:B(b) in the constructor. This variant is useful for defining dependent function application to identifications.

These are given by the following inference rules:

  • Formation rules

    ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x) Γa:AΓb:AΓp:Id A(a,b)ΓfhId x:A.B(x)(f,a,b,p)type\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \; \mathrm{type}}
  • Introduction rules

    ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x) Γa:AΓhrefl x:A.B(x)(f,a):fhId x:A.B(x)(f,a,b,p)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \\ \Gamma \vdash a:A \end{array} }{\Gamma \vdash \mathrm{hrefl}_{x:A.B(x)}(f, a):\mathrm{fhId}_{x:A.B(x)}(f, a, b, p)}
  • Elimination rules

    ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x) Γ,a:A,b:A,p:Id A(a,b),q:fhId x:A.B(x)(f,a,b,p)C(a,b,p,q)type Γt: x:AC(a,a,refl A(a),hrefl x:A.B(x)(f,a)) Γa:AΓb:AΓp:Id A(a,b)Γq:hId x:A.B(x)(f,a,b,p)Γind fhId x:A.B(x)(t,f,a,b,p,q):C(a,b,p,q)\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), q:\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \vdash C(a, b, p, q) \; \mathrm{type} \\ \Gamma \vdash \vdash t:\prod_{x:A} C(a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash q:\mathrm{hId}_{x:A.B(x)}(f, a, b, p) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{fhId}_{x:A.B(x)}}(t, f, a, b, p, q):C(a, b, p, q)}
  • Judgmental computational rule

    ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x) Γ,a:A,b:A,p:Id A(a,b),q:fhId x:A.B(x)(f,a,b,p)C(a,b,p,q)type Γt: x:AC(a,a,refl A(a),hrefl x:A.B(x)(f,a)) Γa:AΓb:AΓp:a= AbΓq:fhId x:A.B(x)(f,a,b,p)Γ,a:Aind fhId x:A.B(x)(t,f,a,a,refl A(a),hrefl x:A.B(x)(f,a))t(a):C(a,a,refl A(a),hrefl x:A.B(x)(f,a))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), q:\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \vdash C(a, b, p, q) \; \mathrm{type} \\ \Gamma \vdash \vdash t:\prod_{x:A} C(a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash q:\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \end{array} }{\Gamma, a:A \vdash \mathrm{ind}_{\mathrm{fhId}_{x:A.B(x)}}(t, f, a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a)) \equiv t(a):C(a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a))}
  • Propositional computational rule

    ΓAtypeΓ,x:AB(x)typeΓf: x:AB(x) Γ,a:A,b:A,p:Id A(a,b),q:fhId x:A.B(x)(f,a,b,p)C(a,b,p,q)type Γt: x:AC(a,a,refl A(a),hrefl x:A.B(x)(f,a)) Γa:AΓb:AΓp:a= AbΓq:fhId x:A.B(x)(f,a,b,p)Γ,a:Aβ hId x:A.B(x)(t,f,a):Id C(a,a,refl A(a),hrefl x:A.B(x)(f,a))(ind fhId x:A.B(x)(t,f,a,a,refl A(a),hrefl x:A.B(x)(f,a)),t(a))\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma \vdash f:\prod_{x:A} B(x) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), q:\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \vdash C(a, b, p, q) \; \mathrm{type} \\ \Gamma \vdash \vdash t:\prod_{x:A} C(a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma \vdash q:\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \end{array} }{\Gamma, a:A \vdash \beta_{\mathrm{hId}_{x:A.B(x)}}(t, f, a):\mathrm{Id}_{C(a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a))}(\mathrm{ind}_{\mathrm{fhId}_{x:A.B(x)}}(t, f, a, a, \mathrm{refl}_A(a), \mathrm{hrefl}_{x:A.B(x)}(f, a)), t(a))}

Given a dependent function f: x:AB(x)f:\prod_{x:A} B(x), we have

hId x:A.B(x)(a,b,p,f(a),f(b))fhId x:A.B(x)(f,a,b,p)\mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b)) \simeq \mathrm{fhId}_{x:A.B(x)}(f, a, b, p)

since by induction we have functions

hIdTofhId(f,a,b,p):hId x:A.B(x)(a,b,p,f(a),f(b))fhId x:A.B(x)(f,a,b,p)\mathrm{hIdTofhId}(f, a, b, p):\mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b)) \to \mathrm{fhId}_{x:A.B(x)}(f, a, b, p)

and

fhIdTohId(f,a,b,p):fhId x:A.B(x)(f,a,b,p)hId x:A.B(x)(a,b,p,f(a),f(b))\mathrm{fhIdTohId}(f, a, b, p):\mathrm{fhId}_{x:A.B(x)}(f, a, b, p) \to \mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b))

inductively defined by

hIdTofhId(f,a,a,refl A(a))(hrefl x:A.B(x)(a,f(a)))hrefl x:A.B(x)(f,a)\mathrm{hIdTofhId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{hrefl}_{x:A.B(x)}(a, f(a))) \equiv \mathrm{hrefl}_{x:A.B(x)}(f, a)

and

fhIdTohId(f,a,a,refl A(a))(hrefl x:A.B(x)(f,a))hrefl x:A.B(x)(a,f(a))\mathrm{fhIdTohId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{hrefl}_{x:A.B(x)}(f, a)) \equiv \mathrm{hrefl}_{x:A.B(x)}(a, f(a))

Thus, we have identifications

H(f,a,b,p):Id fhId x:A.B(x)(f,a,b,p)(hIdTofhId(f,a,b,p)(fhIdTohId(f,a,b,p)(q),q)H(f, a, b, p):\mathrm{Id}_{\mathrm{fhId}_{x:A.B(x)}(f, a, b, p)}(\mathrm{hIdTofhId}(f, a, b, p)(\mathrm{fhIdTohId}(f, a, b, p)(q), q)

and

K(f,a,b,p):Id hId x:A.B(x)(a,b,p,f(a),f(b))(fhIdTohId(f,a,b,p)(hIdTofhId(f,a,b,p)(q)),q)K(f, a, b, p):\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b))}(\mathrm{fhIdTohId}(f, a, b, p)(\mathrm{hIdTofhId}(f, a, b, p)(q)), q)

inductively defined by

H(f,a,a,refl A(a))refl fhId x:A.B(x)(f,a,a,refl A(a))(hrefl x:A.B(x)(f,a))H(f, a, a, \mathrm{refl}_A(a)) \equiv \mathrm{refl}_{\mathrm{fhId}_{x:A.B(x)}(f, a, a, \mathrm{refl}_A(a))}(\mathrm{hrefl}_{x:A.B(x)}(f, a))

and

K(f,a,a,refl A(a))refl hId x:A.B(x)(f,a,a,refl A(a))(hrefl x:A.B(x)(a,f(a))K(f, a, a, \mathrm{refl}_A(a)) \equiv \mathrm{refl}_{\mathrm{hId}_{x:A.B(x)}(f, a, a, \mathrm{refl}_A(a))}(\mathrm{hrefl}_{x:A.B(x)}(a, f(a))

since by the properties of judgmental equality

Id fhId x:A.B(x)(f,a,a,refl A(a))(fhIdTofhId(f,a,a,refl A(a))(hIdTofhId(f,a,a,refl A(a))(hrefl x:A.B(x)(f,a))),hrefl x:A.B(x)(f,a))Id fhId x:A.B(x)(f,a,a,refl A(a))(hrefl x:A.B(x)(f,a)),hrefl x:A.B(x)(f,a))\mathrm{Id}_{\mathrm{fhId}_{x:A.B(x)}(f, a, a, \mathrm{refl}_A(a))}(\mathrm{fhIdTofhId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{hIdTofhId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{hrefl}_{x:A.B(x)}(f, a))), \mathrm{hrefl}_{x:A.B(x)}(f, a)) \equiv \mathrm{Id}_{\mathrm{fhId}_{x:A.B(x)}(f, a, a, \mathrm{refl}_A(a))}(\mathrm{hrefl}_{x:A.B(x)}(f, a)), \mathrm{hrefl}_{x:A.B(x)}(f, a))

and

Id hId x:A.B(x)(a,a,refl A(a),f(a),f(a))(hIdTofhId(f,a,a,refl A(a))(fhIdTohId(f,a,a,refl A(a))(hrefl x:A.B(x)(a,f(a))),hrefl x:A.B(x)(a,f(a)))Id hId x:A.B(x)(a,a,refl A(a),f(a),f(a))(hrefl x:A.B(x)(a,f(a)),hrefl x:A.B(x)(a,f(a)))\mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), f(a), f(a))}(\mathrm{hIdTofhId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{fhIdTohId}(f, a, a, \mathrm{refl}_A(a))(\mathrm{hrefl}_{x:A.B(x)}(a, f(a))), \mathrm{hrefl}_{x:A.B(x)}(a, f(a))) \equiv \mathrm{Id}_{\mathrm{hId}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), f(a), f(a))}(\mathrm{hrefl}_{x:A.B(x)}(a, f(a)), \mathrm{hrefl}_{x:A.B(x)}(a, f(a)))

Then by the properties of quasi-inverse functions and equivalences of types one could prove that both hIdTofhId(f,a,b,p)\mathrm{hIdTofhId}(f, a, b, p) and fhIdTohId(f,a,b,p)\mathrm{fhIdTohId}(f, a, b, p) are equivalences of types.

type, type theory

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

References

Inference rules for heterogeneous identity types (referred to as “dependent identity types” in the article) could be found in section 6 of:

For heterogeneous identity types in the context of higher observational type theory, see:

Last revised on January 25, 2024 at 03:24:00. See the history of this page for a list of all contributions to it.