Re: [HoTT] cubical stacks

[Michael Shulman <shu...@sandiego.edu>]

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.