nLab heterogeneous identity type

Idea

In dependent type theory, a heterogeneous identity type or dependent identity type is a version of the identity type where given a type $A$, a type family $x:A \vdash B(x)$, terms $a:A$, $b:A$, and an identification $p:a =_A b$, the heterogeneous identity type between two elements $y:B(a)$ and $z:B(b)$ is a type whose elements witness that $y$ and $z$ are “equal” over or modulo the identification $p$.

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 type	name of terms
heterogeneous identity type	heterogeneous identities
heterogeneous path type	heterogeneous paths
heterogeneous identification type	heterogeneous identifications
heterogeneous equality type	heterogeneous 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) \vdash \mathrm{Id}_B^p(x, y)$ of the transport equivalence $\mathrm{tr}_B^p:B(a) \simeq B(b)$ on a type family $x:A \vdash B(x)$ and an identification $p:a =_A b$, which is the dependent/heterogeneous version of the identity type for the identity equivalence $\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

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

$$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) \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:

$$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \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:

$$\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:

$$\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:A$ and $b:A$, any identification $p:\mathrm{Id}_A(a,b)$, any elements $y:B(a)$ and $z:B(b)$, and any heterogeneous identification $q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)$ we have a type $C(a, b, p, y, z, q)$, and
2. we have a specified dependent function
   $$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

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

for any $a$, $b$, $p$, $y$, $z$, and $q$.

Then, we have the computation rule or beta-reduction rule. This says that for all elements $a:A$ and $y:B(a)$, substituting the dependent function $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 $a$ and $y$ yields an element equal to $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

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

  $$\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:

$$\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 $A$, a type family $B(x)$ indexed by elements $x:A$, and given a type family $C(a, b, p, y, z, q)$ indexed by elements $a:A$, $b:A$, $p:\mathrm{Id}_A(a, b)$, $y:B(a)$, $z:B(b)$, and $q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)$, for all elements $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:A$, and $y:B(a)$, there exists a unique function $J$ with domain

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

$$\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, \mathrm{refl}_A, y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))$ is equal to $t(a, y)$ in the type $C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, y))$.

From two-type identity types

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

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

Relation between identity types and heterogeneous identity types

There are equivalences between identity types and heterogeneous identity types

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

$$\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:A$, $b:A$, $p:\mathrm{Id}_A(a, b)$, $y:B(a)$, and $z:B(b)$. For constant families $x:A \vdash B$, $\mathrm{transport}_{x:A.B}(a, b, p)(y) \coloneqq y$ and $\mathrm{transport}_{x:A.B}(a, b, p)^{-1}(z) \coloneqq z$, so the above two equivalences simplify down to

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

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

One-to-one correspondence structure

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

• for all elements $z:B(b)$, there exists a unique element $y:B(a)$ such that $\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z)$; the witness is given by the right projection function of transport across $p$, $\mathrm{transport}_{x:A.B(x)}(a, b, p):B(a) \simeq B(b)$

$$\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)$, there exists a unique element $z:B(b)$ such that $\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 $p$, $\mathrm{transport}_{x:A.B(x)}(a, b, p)^{-1}:B(b) \simeq B(a)$

$$\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 $A$, a type family $x:A \vdash B(x)$, and a dependent function $f:\prod_{x:A} B(x)$, there are dependent functions

$$\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:

$$\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.

• The extensionality principle for function types (non-dependent function extensionality) states that there is an equivalence

$$\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:B} \prod_{p:\mathrm{Id}_A(a, b)} \mathrm{hId}_{B}(a, b, p, f(a), g(b))$$

• The extensionality principle for dependent product types (dependent function extensionality) states that there is an equivalence

$$\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:B} \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

$$\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))$$

• The extensionality principle for dependent sum types states that there is an equivalence

$$\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^1$ state that one could construct an element $\mathcal{b}:S^1$ and an identification $\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^1 \vdash C(x)$,

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

• a heterogeneous identification $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^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 $ap$ 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

$$\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:\mathcal{U}$, a judgment $z:\mathcal{T}_\mathcal{U}(A) \vdash B:\mathcal{U}$, terms $x:\mathcal{T}_\mathcal{U}(A)$ and $y:\mathcal{T}_\mathcal{U}(A)$, and an identity $p:\mathrm{id}_{\mathcal{T}_\mathcal{U}(A)}(x,y)$, we have

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

and

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

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

$$\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:\mathcal{U}$

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

See also

type, type theory

• propositions as types, propositions as some types

• inductive type, W-type

• empty type, unit type

• pointed type

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

• dependent sum type, dependent product type

homotopy type, homotopy type theory

• identity type, heterogeneous identity type

• homotopy n-type, connected type

• higher inductive type

• geometric homotopy type, cohesive homotopy type

• two-type identity type

• John Major equality

References

• Mike Shulman, Towards Third-Generation HOTT – Part 1 (slides, video)

• Mike Shulman, Towards Third-Generation HOTT – Part 2 (slides, video)