In this message, I would like to present quickly a generalisation
the groupoid stack model of type theory to a oo-stack model of cubical type theory
(hence of type theory with a hierarchy of univalent universes), which was
made possible by several discussions with Christian Sattler.
This might be interesting since, even classically, it was not known so far if
oo-stacks form a model of type theory with a hierarchy of univalent universes.

  The model is best described as a general method for
building internal models of type theory
(in the style of this paper<https://hal.inria.fr/hal-01441829/document> of Pierre-Marie Pédrot and Nicolas Tabareau,
but for cubical type theory).

 Given a family of types F(c), non necessarily fibrant, over a base type Cov,
we associate the family of (definitional) monads  D_c (X) = X^{F(c)} with
unit maps m_c : X -> D_c(X).
  We say that Cov,F  is a -covering family- iff
each D_c is an idempotent monad, i.e. D_c(m) is path equal to m: D_c(X) -> D_c^2(X).
In this case, we can see Cov as a set of coverings and D_c(X) as the type of descent
data for X for the covering c.
  We define X to be a -stack- iff each map
m_c is an equivalence. It is possible to show that being a stack is preserved
by all operations of cubical type theory, and, using the fact that D_c is idempotent,
that the universe of stacks is itself a stack.
 The following note<http://www.cse.chalmers.se/~coquand/stack.pdf> contains a summary of these discussions, with an example of
a covering family Cov,F.

 Thierry