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 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 contains a summary of these discussions, with an example of

a covering family Cov,F.

 Thierry