Non-wellfounded 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.

翻译：非良基物质集合已由Lindström使用集合胚在Martin-Löf类型论中建模。本文在解释相等为同一类型的同伦类型论（HoTT）中构造了非良基物质集合的模型。第一个模型满足Scott的反基础公理（SAFA），并对迭代集合构造进行对偶化。第二个模型满足Aczel的反基础公理（AFA），通过将Aczel-Mendler终余代数定理适配到类型论（需要命题缩放）而构造。为将余代数理论与反基础公理扩展到更高类型层次，我们制定了AFA和SAFA的推广形式，并构造了满足SAFA推广的模型层级。这些推广基于两位作者先前发展的单值物质集合论框架。由于模型构造基于M类型，本文还将M类型的同一类型刻画为索引M类型。我们的结果已在证明助手Agda中形式化。