一句话：在同伦类型论中构造满足 SAFA 与 AFA 的非良基集合模型，并推广反基础公理与 M-类型 identity type 刻划。
本文在同伦类型论（HoTT）中以 identity type 解释相等，构造非良基具体集合的模型。此前 Lindström 用 setoid 在 Martin-Löf 类型论中建模。第一个 HoTT 模型满足 Scott 反基础公理（SAFA），由迭代集合构造对偶得到；第二个满足 Aczel 反基础公理（AFA），通过将 Aczel–Mendler 终结余代数定理适配到类型论，并需要命题重设。作者进一步推广 AFA 与 SAFA 到更高类型层级，基于 Univalent Material Set Theory 构造满足 SAFA 推广的一族模型，并刻划 M-类型的 identity type 为索引 M-类型。所有结果在 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GylterudSV26,
title = {Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory},
author = {Hakon Robbestad Gylterud and Elisabeth Stenholm and Niccolò Veltri},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:35)2026}
}