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

文章基本信息

  • 标题:CANONICITY AND HOMOTOPY CANONICITY FOR CUBICAL TYPE THEORY
  • 本地全文:下载
  • 作者:Thierry Coquand ; Simon Huber ; Christian Sattler
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2022
  • 卷号:18
  • 期号:1
  • 页码:1-35
  • DOI:10.46298/lmcs-18(1:28)2022
  • 语种:English
  • 出版社:Technical University of Braunschweig
  • 摘要:Cubical type theory provides a constructive justification of homotopy type theory. 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. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
  • 关键词:cubical type theory;univalence;canonicity;sconing;Artin glueing
国家哲学社会科学文献中心版权所有