nLab boundary separation

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

…

See also

• uniqueness of identity proofs

• axiom K

References

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).