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
XTT is an set-level cubical type theory developed by Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. The authors have stated that the name is not short for anything, but it is a pun on “eXtensional Type Theory”.
XTT features boundary separation, which implies UIP as a theorem of XTT, rather than an axiom as in Martin-Löf type theory. As a result, it is an example of a cubical type theory which is not a homotopy type theory.
Additionally, XTT has regularity, canonicity, and certain higher inductive types like propositional truncation. It is an open question if it additionally has decidable type checking and normalization.
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers (ed.), 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 March 2, 2023 at 12:09:08. See the history of this page for a list of all contributions to it.