[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Heterogeneous identity types: There are many different ways to define heterogeneous identity types using [[inference rules]]. The simplest definition, which doesn't require any other types to be defined except for [[identity types]], 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)$$ Heterogeneous identity types, like [[function types]] and [[pair types]], come in dependent and non-dependent versions. Here, the default heterogeneous identity types are the dependent heterogeneous identity types. The non-dependent heterogeneous identity types are simply dependent heterogeneous identity types for which the type family $x:A \vdash B(x)$ is a constant type family; i.e. for which $B(a)$ and $B(b)$ are [[judgmentally equal]] to each other for all $a:A$ and $b:A$, and are written as $\mathrm{hId}_{B}(a, b, p, y, z)$ to indicate that the type family is constant. For simplicity, only the inference rules for dependent heterogeneous identity types are given. ### Inference rules The inference rules for forming heterogeneous identity types and terms in [[Martin-Löf dependent type theory]] are as follows (expressed in [[sequent calculus]]). First the inference rule that defines the heterogeneous identity type itself, as a [[dependent type]], in some [[context]] $\Gamma$. **[[type formation]]** $$\frac{\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) \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. **[[term introduction]]** $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}} {\Gamma, 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)}$$ The element $\mathrm{hrefl}_{x:A.B(x)}(a, y)$ is called heterogeneous reflexivity, similar to how in vanilla identity types, the element $\mathrm{refl}_A(a)$ is [[reflexivity]]. Then we have the "elimination" rule: **[[term elimination]]** $$\frac{\begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma, a:A, b:A, p:Id_A(a,b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), \Delta(a, b, p, y, z, q) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma, a:A, y:B(a), \Delta(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \vdash t : C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \end{array} } {\Gamma, a:A, b:A, p:Id_A(a,b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), \Delta(a, b, p, y, z, q) \vdash J(t;a, b, p, y, z, q) : C(a, b, p, y, z, q)}$$ Ignore the presence of the additional context $\Delta$ for now; it is unnecessary if we also have [[dependent product type]]s. 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 1. for all elements $a:A$ and $y:B(a)$, we have a specified term $t: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 $J(t;a,b,p,y,z,q):C(a,b,p,y,z,q)$ for *any* $a$, $b$, $p$, $y$, $z$, and $q$. Finally, we have the "computation" or [[β-reduction]] rule. This says that if we substitute along heterogeneous [[reflexive relation|reflexivity]], nothing happens. There are two possible computation rules, which result in strict and weak heterogeneous identity types respectively **[[computation rule]] for strict 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:Id_A(a,b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), \Delta(a, b, p, y, z, q) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma, a:A, y:B(a), \Delta(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \vdash t : C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \end{array} } {\Gamma, a:A, y:B(a), \Delta(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \vdash J(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \equiv t:C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))}$$ The computation rules for strict heterogeneous identity types state that the element $$J(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))$$ is [[judgmentally equal]] to $t$ in the type $$C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))$$ **[[computation rule]] for weak 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:Id_A(a,b), y:B(a), z:B(b), q:\mathrm{hId}_{x:A.B(x)}(a, b, p, y, z), \Delta(a, b, p, y, z, q) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma, a:A, y:B(a), \Delta(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \vdash t : C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \end{array} } {\Gamma, a:A, y:B(a), \Delta(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)) \vdash \beta(a, y):\mathrm{Id}_{C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))}(J(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y)), t)}$$ The computation rules for weak heterogeneous identity types state that the element $$J(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))$$ is only [[typally equal]] to $t$ in the type $$C(a, a, \mathrm{refl}_A(a), y, y, \mathrm{hrefl}_{x:A.B(x)}(a, a, \mathrm{refl}_A(a), y, y))$$ There is also the [[uniqueness rules]] or [[eta-reduction]] rules. However, similarly to those of the identity type, the uniqueness rules are usually not included in the inference rules for heterogeneous identity types, because strict or judgmental uniqueness rules for heterogeneous identity types implies the [[reflection rule]] and results in an [[extensional type theory]], and weak or typal uniqueness rules for heterogeneous identity types are already provable from the other inference rules for heterogeneous identity types. \section{Old section} Heterogeneous identity types, like function types and pair types, come in dependent and non-dependent flavors. This is because the usual natural deduction rules for dependent heterogeneous identity types require a type $A$ and a type family $x:A \vdash B(x)$; the non-dependent version is for a constant family $B$, which is just a type $B$; the dependent function $f:\prod_{x:A} B(x)$ in the rules for the dependent heterogeneous identity type becomes the non-dependent function $f:A \to B$ in the non-dependent heterogeneous identity types. The introduction rules for dependent and non-dependent heterogeneous identity types result in the [[dependent function application to identifications]] and non-dependent [[function application to identifications]] respectively, in the same way that the introduction rules for [[identity types]] result in reflexivity. Finally, as with every other type in [[dependent type theory]], the [[computation rules]] of both dependent and non-dependent heterogeneous identity types use [[judgmental equality]], [[propositional equality]], or [[typal equality]]. ### Inference rules for non-dependent heterogeneous identity types In the same way that there are [[inference rules]] for non-dependent function types and non-dependent pair types, there are also rules for non-dependent heterogeneous identity types, where the type family $B$ is a constant type family. Formation rule for non-dependent heterogeneous identity types: $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \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 \quad \Gamma \vdash z:B \end{array} }{\Gamma \vdash \mathrm{hId}_B(a, b, p, y, z) \; \mathrm{type}}$$ Introduction rule for non-dependent heterogeneous identity types: $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{ap}_B(f, a, b, p):\mathrm{hId}_B(a, b, p, f(a), f(b))}$$ Elimination rule for non-dependent heterogeneous identity types: $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \quad \Gamma \vdash q:\mathrm{hId}_B(a, b, p, y, z) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, y, z, q):C(a, b, p, y, z, q)}$$ Computation rules for non-dependent heterogeneous identity types: * Judgmental computational rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \equiv t(f, a, b, p):C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p))}$$ * Propositional computational rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \equiv_{C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p))} t(f, a, b, p) \; \mathrm{true}}$$ * Typal computational rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \beta_{\mathrm{hId}_B}(t, f, a, b, p):\mathrm{Id}_{C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p))}(\mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)), t(f, a, b, p))}$$ Uniqueness rule for non-dependent heterogeneous identity types: * Judgmental uniqueness rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \quad \Gamma \vdash q:\mathrm{hId}_B(a, b, p, y, z) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, y, z, q) \equiv r:C(a, b, p, y, z, q)}$$ * Propositional uniqueness rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \quad \Gamma \vdash q:\mathrm{hId}_B(a, b, p, y, z) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, y, z, q) \equiv_{C(a, b, p, y, z, q)} r \; \mathrm{true}}$$ * Typal uniqueness rules $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{ap}_B(f, a, b, p)) \\ \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \quad \Gamma \vdash y:B \quad \Gamma \vdash z:B \quad \Gamma \vdash q:\mathrm{hId}_B(a, b, p, y, z) \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_B(a, b, p, y, z) \vdash r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \eta_{\mathrm{hId}_B}(t, a, b, p, y, z, q, r):\mathrm{Id}_{C(a, b, p, y, z, q)}(\mathrm{ind}_{\mathrm{hId}_B}(t, a, b, p, y, z, q), r)}$$ Similar to the case for [[identity types]], having the judgmental or propositional uniqueness rules for non-dependent heterogeneous identity types implies that the type theory is an [[extensional type theory]]. The typal uniqueness rules for non-dependent heterogeneous identity types is always provable from the other four inference rules. The elimination, typal computation, and typal uniqueness rules for non-dependent heterogeneous identity types state that non-dependent heterogeneous identity types satisfy the **dependent universal property of non-dependent 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 non-dependent heterogeneous identity types could be simplified to the following rule: $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \\ \Gamma, a:A, b:A, p:\mathrm{Id}_A(a, b), y:B, z:B, q:\mathrm{hId}_{B}(a, b, p, y, z) \vdash C(a, b, p, y, z, q) \; \mathrm{type} \\ \Gamma \vdash t:\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p)) \\ \Gamma \vdash f:A \to B \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{up}_{\mathrm{hId}_{B}}(t, f, a, b, p): \begin{array}{c} \exists!J:\left(\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p))\right) \\ \to \left(\prod_{c:A} \prod_{d:A} \prod_{r:\mathrm{Id}_A(c, d)} \prod_{e:B} \prod_{f:B} \prod_{s:\mathrm{hId}_{B}(c, d, r, e, f)} C(c, d, r, e, f, s)\right) \\ .\mathrm{Id}_{C(a, b, p, f(a), f(b))}(J(t, a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p)), t(f, a, b, p)) \end{array} }$$ In natural language this states that given types $A$ and $B$, 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$, $z:B$, and $q:\mathrm{hId}_{B}(a, b, p, y, z)$, for all elements $t:\prod_{f:A \to B}$, $a:A$, $b:A$, and $p:\mathrm{Id}_A(a, b)$, there exists a unique function $J$ with domain $$\prod_{f:A \to B} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p))$$ and codomain $$\prod_{c:A} \prod_{d:A} \prod_{r:\mathrm{Id}_A(c, d)} \prod_{e:B} \prod_{f:B} \prod_{s:\mathrm{hId}_{B}(c, d, r, e, f)} C(c, d, r, e, f, s)$$ such that $J(t, a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p))$ is equal to $t(f, a, b, p)$ in the type $C(a, b, p, f(a), f(b), \mathrm{apd}_{B}(f, a, b, p))$. ### Inference rules for dependent heterogeneous identity types Formation rule for dependent 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}}$$ Introduction rule for dependent heterogeneous identity types: $$\frac{ \begin{array}{l} \Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{apd}_{x:A.B(x)}(f, a, b, p):\mathrm{hId}_{x:A.B(x)}(a, b, p, f(a), f(b))}$$ Elimination rule for dependent 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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \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)}$$ Computation rules for dependent heterogeneous identity types: * Judgmental computational rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \equiv t(f, a, b, p):C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))}$$ * Propositional computational rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \equiv_{C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))} t(f, a, b, p) \; \mathrm{true}}$$ * Typal computational rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \beta_{\mathrm{hId}_{x:A.B(x)}}(t, f, a, b, p):\mathrm{Id}_{C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))}(\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)), t(f, a, b, p))}$$ Uniqueness rule for dependent heterogeneous identity types: * Judgmental uniqueness rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \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) \\ \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 r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, y, z, q) \equiv r:C(a, b, p, y, z, q)}$$ * Propositional uniqueness rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \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) \\ \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 r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, y, z, q) \equiv_{C(a, b, p, y, z, q)} r \; \mathrm{true}}$$ * Typal uniqueness rules $$\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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \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) \\ \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 r:C(a, b, p, y, z, q) \end{array} }{\Gamma \vdash \eta_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, y, z, q, r):\mathrm{Id}_{C(a, b, p, y, z, q)}(\mathrm{ind}_{\mathrm{hId}_{x:A.B(x)}}(t, a, b, p, y, z, q), r)}$$ Similar to the case for [[identity types]] and non-dependent heterogeneous identity types, having the judgmental or propositional uniqueness rules for dependent heterogeneous identity types implies that the type theory is an [[extensional type theory]]. The typal uniqueness rules for dependent heterogeneous identity types is always provable from the other four inference rules. The elimination, typal computation, and typal uniqueness rules for dependent heterogeneous identity types state that dependent heterogeneous identity types satisfy the **dependent universal property of dependent 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 dependent 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_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)) \\ \Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:\mathrm{Id}_A(a, b) \end{array} }{\Gamma \vdash \mathrm{up}_{\mathrm{hId}_{x:A.B(x)}}(t, f, a, b, p): \begin{array}{c} \exists!J:\left(\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))\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, b, p, f(a), f(b))}(J(t, a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p)), t(f, a, b, p)) \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_{f:\prod_{x:A} B(x)}$, $a:A$, $b:A$, and $p:\mathrm{Id}_A(a, b)$, there exists a unique function $J$ with domain $$\prod_{f:\prod_{x:A} B(x)} \prod_{a:A} \prod_{b:A} \prod_{p:\mathrm{Id}_A(a, b)} C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))$$ 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, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))$ is equal to $t(f, a, b, p)$ in the type $C(a, b, p, f(a), f(b), \mathrm{apd}_{x:A.B(x)}(f, a, b, p))$. category: redirected to nlab