Re: [HoTT] cubical stacks

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

I think it is sort of the opposite.  Here we are seeing the oo-exact
completion of a 1-category, whereas they start with an (oo,1)-category
and construct the 1-exact completion of its homotopy 1-category in a
"homotopy" way.

On Sun, May 14, 2017 at 12:44 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> 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.
>
>