论文标题
终末煤膜和非偏开的集合集合型理论
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
论文作者
论文摘要
使用setoids通过Lindström在Martin-Löf类型理论中对非曲折的材料集进行了建模。在本文中，我们在同型类型理论（HOTT）中构建了非曲折材料集的模型，其中平等被解释为身份类型。第一个模型满足了Scott的抗创始公理（SAFA），并双重地构建了迭代套件。第二个模型满足了Aczel的抗创始公理（AFA），并通过适应Aczel--Mendler的末端煤层定理来构建型理论，该理论需要调整命题大小。 为了将煤层理论和抗创始公理扩展到更高的类型水平，我们制定了AFA和SAFA的概括，并构建了满足Safa概括的模型的层次结构。这些概括建立在单位材料集理论的框架上，这是由两位作者开发的。 由于模型构造基于M型，因此本文还包括将M型的身份类型作为索引M型的表征。 我们的结果是在证明AGDA中正式化的。
Non-wellfounded material sets have been modeled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as the identity type. The first model satisfies Scott's Anti-Foundation Axiom (SAFA) and dualises the construction of iterative sets. The second model satisfies Aczel's Anti-Foundation Axiom (AFA), and is constructed by adaption of Aczel--Mendler's terminal coalgebra theorem to type theory, which requires propositional resizing. In an bid to extend coalgebraic theory and anti-foundation axioms to higher type levels, we formulate generalisations of AFA and SAFA, and construct a hierarchy of models which satisfies the SAFA generalisations. These generalisations build on the framework of Univalent Material Set Theory, previously developed by two of the authors. Since the model constructions are based on M-types, the paper also includes a characterisation of the identity type of M-types as indexed M-types. Our results are formalised in the proof-assistant Agda.
