Contents

Contents

Idea

Boundary separation is a modular reconstruction of the uniqueness of identity proofs in cubical type theory. It is a rule which implies UIP as a theorem.

Definition

Recall that in cubical type theory, there is an interval primitive $I$ with endpoints $0:I$ and $1:I$, as well as face formulas $\phi:F$ with rules which make $\phi$ behave like a formula in first-order logic ranging over the interval $I$.

Boundary separation is the following rule:

$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash r:I \quad \Gamma, \partial(r) \vdash a \equiv b:A}{\Gamma \vdash a \equiv b:A}$

where $I$ is the interval primitive in cubical type theory and $\partial(r)$ is the boundary face formula for dimension variables:

$\delta(r) \coloneqq r = 0 \vee r = 1$

(The interval primitive $I$ has more points than $0$ and $1$, so it is not the case that the sequent $r:I \vdash r = 0 \vee r = 1 \;\mathrm{true}$ holds.)

There is also a typal version of boundary separation which refers to cubical path types rather than definitional equality, given by the following rule:

$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash r:I \quad \Gamma, \partial(r) \vdash p:a =_A b}{\Gamma \vdash p:a =_A b}$

Proof of UIP from boundary separation

We denote path types by $a =_A b$ and dependent path types by $a =_{i.A} b$.

Consider the following context:

$\Gamma \coloneqq (\Delta, A \; \mathrm{type}, a:A, b:A, p:a =_{A} b, q: a =_A b)$