2026-07-24T11:53:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10538 2024-03-12T11:57:27Z ddc:004 open_access

Cubical Syntax for Reflection-Free Extensional Equality Sterling, Jonathan Angiuli, Carlo Gratzer, Daniel Dependent type theory extensional equality cubical type theory categorical gluing canonicity We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jonathan Sterling and Carlo Angiuli and Daniel Gratzer 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.31 urn:nbn:de:0030-drops-105387 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31 eng https://creativecommons.org/licenses/by/3.0/legalcode