首页    期刊浏览 2024年11月05日 星期二
登录注册

文章基本信息

  • 标题:Homotopy Canonicity for Cubical Type Theory
  • 本地全文:下载
  • 作者:Thierry Coquand ; Simon Huber ; Christian Sattler
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2019
  • 卷号:131
  • 页码:1-23
  • DOI:10.4230/LIPIcs.FSCD.2019.11
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.
  • 关键词:cubical type theory; univalence; canonicity; sconing; Artin glueing
国家哲学社会科学文献中心版权所有