终端余代数与同伦类型理论中的非良基础集
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
AI总结：
本文在同伦类型理论中构建了非良基础集模型，提出扩展AFA和SAFA的通用化，并通过M型构建了满足SAFA通用化的层级模型，同时刻画了M型的身份类型。
摘要：
非良基础材料集在马丁-洛夫类型理论中通过setoids被建模。本文在同伦类型理论（HoTT）中构造了非良基础材料集模型，其中等价性被解释为恒等类型。第一个模型满足斯科特的反基础公理（SAFA）并双倍迭代集的构造。第二个模型满足阿克泽的反基础公理（AFA），并通过将阿克泽-梅尔德的终端余代数定理适应到类型理论中构建，这需要命题大小化。为扩展余代数理论和反基础公理到更高类型级别，本文提出了AFA和SAFA的通用化，并构建了一个满足SAFA通用化的模型层级。这些通用化基于Univalent Material Set Theory框架，此前由两位作者开发。由于模型构造基于M-types，本文还包含对M-types身份类型的刻画作为索引M-types。本文结果在证明助手Agda中正式化。
英文摘要：
Non-well-founded material sets have been modelled 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
