cubical stacks

cubical stacks

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 1559 bytes --]

 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<https://hal.inria.fr/hal-01441829/document> 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<http://www.cse.chalmers.se/~coquand/stack.pdf> contains a summary of these discussions, with an example of
a covering family Cov,F.

 Thierry

[-- Attachment #2: Type: text/html, Size: 2481 bytes --]

Re: [HoTT] cubical stacks

[Michael Shulman]

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.

Re: [HoTT] cubical stacks

[Thierry Coquand]

[-- Attachment #1: Type: text/plain, Size: 6696 bytes --]


Many thanks for the question and the comment.

 After I sent my message, I realised that the note can be seen as a (new) example
of the situation you described in

http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf

and which has been formalised in

 https://hott.github.io/HoTT/coqdoc-html/HoTT.Modalities.Lex.html

and in the work

 https://jfr.unibo.it/article/view/6232

 The point is that one can apply this technique to presheaf models
of cubical type theory. (Note that they are not examples of “open” modality in general
since one does exponentiation w.r.t. a cubical presheaf which may not be
fibrant.) And this is possible since the cubical set model generalise directly
to the general presheaf case (contrary to the simplicial set model).

 For question 1, indeed, we have looked only at special “extreme” cases
precisely in order to address the issue you mention:
 -when the space is “connected” (e.g. unit interval) where the constant presheaf
N already satisfies the stack condition, and
 -when the space is totally disconnected (e.g. Cantor space) where we need to impose
an extra condition (to have an inverse of the m map for this kind of covering which is strictly
right inverse) in order to interpret the elimination rule in a strict way.

 Note that one can combine the two conditions: for instance, the case the space
which is the product of the unit interval and Cantor space
or the case of a site used to interpret constructively the algebraic closure of a field (which
is the site of etale algebra over the field where a cover is either disconnected
given by an idempotent element of the algebra, or connected given by a
separable algebraic extension).


 For comment 2, this is related to the remark you made ~ 1 year ago
that the type of h-propositions in the presheaf  model  is not equivalent to the
to the presheaf of truth-values \Omega.
It is indeed possible to prove this with the following example. If one considers
the poset

       w
   /       \
 w0    w1
   \       /
     w01

the presheaf model over this poset has classically the following 6 truth-values
(classically there are only 2 truth values 0 and 1), which describe \Omega

w: 0     w0 : 0     w1 :0    w01 : 0
w: 0     w0 : 0     w1 :0    w01 : 1
w: 0     w0 : 1     w1 :0    w01 : 1
w: 0     w0 : 0     w1 :1    w01 : 1
w: 0     w0 : 1     w1 :1    w01 : 1
w: 1     w0 : 1     w1 :1    w01 : 1

 If we consider in this model the groupoid G which is empty at level w, has a point a0 at level
w0, a point a1 at level w1 and a path a0 -> a1 at level w01, this groupoid
G is a proposition which is not equivalent to any of these propositions in \Omega,
and so (since the cubical nerve of this groupoid is fibrant in the model) this shows that
the canonical map

\Omega   ------->       hProp(U) = Sigma (X:U) isProp X

is not an equivalence. (This is to be compared with the situation for the corresponding
injective simplicial model structure where, surprisingly,  the nerve of G is not fibrant.)

 I was thinking of  fibrant cubical pre sheaves as pre sheaves of oo-groupoids
(since one can think of a fibrant cubical set as an oo-groupoid), hence I mentioned
"oo-stacks” but this should be avoided if, as you write,
what is described is too far from the standard notion oo-stacks.

 I only hope that the note gives some examples of “sheaf" models  of
type theory with the axiom of univalence, which can be used in the same way
sheaf models are used for higher order logic.



On 14 May 2017, at 11:53, Michael Shulman <shu...@sandiego.edu<mailto: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<mailto: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<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.


[-- Attachment #2: Type: text/html, Size: 11059 bytes --]

Re: [HoTT] cubical stacks

[Bas Spitters]

[-- Attachment #1: Type: text/plain, Size: 3734 bytes --]

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.
>

[-- Attachment #2: Type: text/html, Size: 4881 bytes --]

Re: [HoTT] cubical stacks

[Michael Shulman]

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.
>
>