  Non-wellfounded material sets have previously been modeled in Martin-L\"of
type theory by Lindstr\"om 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.
