文章基本信息

标题：A CUBICAL LANGUAGE FOR BISHOP SETS
本地全文：下载
作者：Jonathan Sterling ; Carlo Angiuli ; Daniel Gratzer 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2022
卷号：18
期号：1
页码：1-80
DOI：10.46298/lmcs-18(1:43)2022
语种：English
出版社：Technical University of Braunschweig
摘要：We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.
关键词：cubical type theory;Bishop sets;proof irrelevance;Artin gluing;logical predicates