Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Sterling, Jonathan; Angiuli, Carlo; Gratzer, Daniel http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-105387
URL:

; ;

Cubical Syntax for Reflection-Free Extensional Equality

pdf-format:


Abstract

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.

BibTeX - Entry

@InProceedings{sterling_et_al:LIPIcs:2019:10538,
  author =	{Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
  title =	{{Cubical Syntax for Reflection-Free Extensional Equality}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{31:1--31:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10538},
  URN =		{urn:nbn:de:0030-drops-105387},
  doi =		{10.4230/LIPIcs.FSCD.2019.31},
  annote =	{Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity}
}

Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity
Seminar: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue date: 2019
Date of publication: 2019


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI