natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
basic constructions:
strong axioms
further
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.
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:
where $I$ is the interval primitive in cubical type theory and $\partial(r)$ is the boundary face formula for dimension variables:
(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:
We denote path types by $a =_A b$ and dependent path types by $a =_{i.A} b$.
Consider the following context:
…
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).
Last revised on January 25, 2023 at 13:27:58. See the history of this page for a list of all contributions to it.