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

文章基本信息

  • 标题:Non-Wellfounded Trees in Homotopy Type Theory
  • 本地全文:下载
  • 作者:Benedikt Ahrens ; Paolo Capriotti ; R{\'e}gis Spadotti
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:38
  • 页码:17-30
  • DOI:10.4230/LIPIcs.TLCA.2015.17
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We prove a conjecture about the constructibility of conductive types - in the principled form of indexed M-types - in Homotopy Type Theory. The conjecture says that in the presence of inductive types, coinductive types are derivable. Indeed, in this work, we construct coinductive types in a subsystem of Homotopy Type Theory; this subsystem is given by Intensional Martin-Löf type theory with natural numbers and Voevodsky's Univalence Axiom. Our results are mechanized in the computer proof assistant Agda.
  • 关键词:Homotopy Type Theory; coinductive types; computer theorem proving; Agda
国家哲学社会科学文献中心版权所有