  Homotopy type theory (HoTT) can be seen as a generalisation of structural set
theory, in the sense that 0-types represent structural sets within the more
general notion of types. For material set theory, we also have concrete models
as 0-types in HoTT, but this does not currently have any generalisation to
higher types. The aim of this paper is to give such a generalisation of
material set theory to higher type levels within homotopy type theory. This is
achieved by generalising the construction of the type of iterative sets. At
level 1, this gives a connection between groupoids and multisets.
  More specifically, we define the notion of an $\in$-structure as a type with
an extensional binary type family and generalise the axioms of constructive set
theory to higher type levels. Once an $\in$-structure is given, its elements
can be seen as representing types in the ambient type theory.
  The theory has an alternative, coalgebraic formulation, in terms of
coalgebras for a certain hierarchy of functors, $P^n$, which generalises the
powerset functor from sub-types to covering spaces and $n$-connected maps in
general. The coalgebras which furthermore are fixed-points of their respective
functors in the hierarchy are shown to model the axioms given in the first
part.
  As concrete examples of models for the theory developed we construct the
initial algebras of the $P^n$ functors. In addition to being an example of
initial algebras of non-polynomial functors, this construction allows one to
start with a univalent universe and get a hierarchy of $\in$-structures which
gives a stratified $\in$-structure representation of that universe. These types
are moreover $n$-type universes of $n$-types which contain all the usual types
an type formers.
