Contents

# Contents

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