Thanks Mike. This is very informative.

Is your oo-exact completion related to the homotopy exact completion by
Benno and Ieke?
https://arxiv.org/abs/1603.02456

On Sun, May 14, 2017 at 11:53 AM, Michael Shulman <shu...@sandiego.edu>
wrote:

> 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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>