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

文章基本信息

  • 标题:For Finitary Induction-Induction, Induction Is Enough
  • 本地全文:下载
  • 作者:Ambrus Kaposi ; András Kovács ; Ambroise Lafont
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:175
  • 页码:1-30
  • DOI:10.4230/LIPIcs.TYPES.2019.6
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.
  • 关键词:type theory; inductive types; inductive-inductive types
国家哲学社会科学文献中心版权所有