boundary separation (changes) in nLab

Showing changes from revision #4 to #5: Added | Removed | Changed

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 II with endpoints 0:I0:I and 1:I1:I, as well as face formulas ϕ:F\phi:F with rules which make ϕ\phi behave like a formula in first-order logic ranging over the interval II.

Boundary separation is the following rule:

Γ⊢AtypeΓ⊢r:IΓ,∂(r)⊢a≡b:AΓ⊢a≡b:A\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 II is the interval primitive in cubical type theory and ∂(r)\partial(r) is the boundary face formula for dimension variables:

δ(r)≔r=0∨r=1\delta(r) \coloneqq r = 0 \vee r = 1

(The interval primitive II has more points than 00 and 11, so it is not the case that the sequent r:I⊢r=0∨r=1truer: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:

Γ⊢AtypeΓ⊢a:AΓ⊢b:AΓ⊢r:IΓ,∂(r)⊢p:a= AbΓ⊢p:a= Ab\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= Aba =_A b and dependent path types by a= i.Aba =_{i.A} b.

Consider the following context:

Γ≔(Δ,Atype,a:A,b:A,p:a= Ab,q:a= Ab)\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).