nLab dependent identity type

Idea

In dependent type theory, given a type $A$, a type family $x:A \vdash B(x)$, terms $a_0:A$, $a_1:A$, and an identification $p:a_0 =_A a_1$, a dependent identity type or a heterogeneous identity type between two elements $b_0: B(a_0)$ and $b_1:B(a_1)$ is a type whose elements witness that $b_0$ and $b_1$ are “equal” over or modulo the identification $p$. There are different ways to define this precisely, depending partly on the particular type theory used.

Definition in Martin-Löf type theory

One way to define the dependent identity type in Martin-Lof type theory is using transport along the identification $p$:

$$(a =_B^p b) \coloneqq (\mathrm{tr}_B^p(a) =_{B(b)} b)$$

There are also other possibilities…

Definition in higher observational type theory

In higher observational type theory, the dependent 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 dependent identity type then depends on an “identification in that telescope”, which is defined by mutual recursion as a telescope of dependent 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

Dependent 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 dependent 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)$$

Categorical semantics

needs to be written

See also

type, type theory

• propositions as 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, dependent identity type

• homotopy n-type, connected type

• higher inductive type

• geometric homotopy type, cohesive homotopy type

References

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

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