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

文章基本信息

  • 标题:A Model of Type Theory in Cubical Sets
  • 本地全文:下载
  • 作者:Marc Bezem ; Thierry Coquand ; Simon Huber
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2014
  • 卷号:26
  • 页码:107-128
  • DOI:10.4230/LIPIcs.TYPES.2013.107
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
  • 关键词:Models of dependent type theory; cubical sets; Univalent Foundations
国家哲学社会科学文献中心版权所有