equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
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
Cubical path types are a form of path types in dependent type theory used in cubical type theories.
A major difference between cubical path types and Martin-Löf identity types is the behaviour of the J rule. In Martin-Löf identity types the J rule holds up to definitional equality, but for cubical path types, the J rule only holds up to a path.
Another difference is that transport generally behaves better with cubical path types. Certain rules for the computation of transports in concrete type families hold up to definitional equality for cubical path types, but only up to an identification for Martin-Löf identity types.
The rules for (dependent) cubical path types are as follows
In addition, there are coercion and composition operations which make the path type behave like an identity type:
…
In general, cubical path types in cubical type theory do not satisfy the J rule definitionally. However one could force the J rule to hold definitionally by appending a coercion regularity rule:
to the type theory.
On why cubical path types and Martin-Löf identity types are different:
On cubical path types in XTT:
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 December 8, 2023 at 19:00:45. See the history of this page for a list of all contributions to it.