This is very nice.  I have two questions/comments:

1. I would not expect the "stack" model to inherit inductive types
like coproducts, natural numbers objects, W-types, and HITs with
judgmental computation rules.  In general I don't think these
operations will preserve stacks, and you can apply the monad to
stackify them but the result will only inherit a universal property up
to equivalence within stacks.  Is that right?

2. I agree that the word "stack" is appropriate for the internal
construction, which is a categorification of Lawvere-Tierney sheaves,
for which the word "sheaf" is often used.  However, when performed
inside the "cubical presheaves on a space" model, I don't believe it
produces oo-stacks in the usual sense of the external set theory,
because "cubical presheaves on a space" with this sort of "pointwise
homotopy theory" don't present the homotopy theory of oo-presheaves on
that space, at least not without some extra fibrancy condition.  I
think they are better regarded as a sort of "oo-exact completion" of
the 1-category of presheaves.

On Thu, May 4, 2017 at 10:31 AM, Thierry Coquand
<Thierry...@cse.gu.se> wrote:
>  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 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
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.