From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.218.199 with SMTP id c190mr1357809ywe.101.1494791082872; Sun, 14 May 2017 12:44:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.37.68 with SMTP id l65ls3371528iol.5.gmail; Sun, 14 May 2017 12:44:42 -0700 (PDT) X-Received: by 10.99.102.69 with SMTP id a66mr1335052pgc.89.1494791082031; Sun, 14 May 2017 12:44:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1494791081; cv=none; d=google.com; s=arc-20160816; b=INGOQr3PXEujmvxEICBe1Eh30+/AaODK0P3EUkvJ9pWGBxQq9LKKKpyT9YdkcLyF7e 7Lp81t3hdxCKThKeGq0bEXlXXBsRLae8lSgr43203RbBkQOMbWSAw39Bm60V7mf/DB6B 2AWnbu8VTOl49RQ65g3YIVG2HNRyIIUzEjPdS5y3yWpLm4lv4BU3Rr836Hm5mg6bFjb/ kyXIcZT397BoVYzdQDVG8vo4E+8ZcRgkOrpuGkVW+D4q/eFQGbMnYaLy4JY+uB3YCMTe IjuPwSmgYIou1HnBCd/SMIaSeer27Q7zFAySueKJ3wJ8yxHcGjWqcHpM2XrNem6+e7vn kAvA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=wyqY/5JUG51xH0nsb9P+lTGflikDAlbklZ7FaMpKdWo=; b=An38BAJdemFmUNU4ZQQV1Zp6YZtSfKfpiGWquyVTEEmbSyganjz68aeF6hyPxmvou/ FFZXbjZFxOnbMW9uwEpJpLwsJLK+lk2eZC9eqzyB2bbWymv43P6Y4+Y3AKWv0+Etxgyf Lu+Kw0dNK4SoCcJGfjd4EYNf6oXMLPR7SGGY3KWffZgnek/AP9oVZbzesAlVFZgbvZm5 zZSBftUdSwW0J+suPi/ZNi39Pr/WEsHKxzi5/H+30ZD5yf/sau1wJtMmMkUy23GeDVL/ thTsI4puWvcK4Apkn+Jrv7EzZrGBpXSc6VT7LSkqOe/68QdXsRgSqbO1uUQGPXlZ3suN +fMA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x231.google.com (mail-ua0-x231.google.com. [2607:f8b0:400c:c08::231]) by gmr-mx.google.com with ESMTPS id i17si546224vkd.2.2017.05.14.12.44.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 14 May 2017 12:44:41 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) client-ip=2607:f8b0:400c:c08::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x231.google.com with SMTP id g49so68548041uaa.1 for ; Sun, 14 May 2017 12:44:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=wyqY/5JUG51xH0nsb9P+lTGflikDAlbklZ7FaMpKdWo=; b=doz2Vciq9BT3rTFWq14UYZMj7O+WK0ypsFDHDShJmYzz1NsGa1+rCZ3CUGsT03Vv6y 5h3Ltz2N1+fxlzcuJl/s6rLv/rCDr8HPhe2QklQ+qT9M4QagJAzjBBLDUCXlNo5oWTGT 4NqezvM0xrd4yZ9oW0ffFNdCdm8abEJmh1yEqnLb5mywesEbt3oadWRYemciIBPYmBmP YvPUsaT91EAB8BBN8MrOJD4wrxLc6qZLXCju3vE/wy8WTac3gQxsrBxgepIas608g7eP 8RzCBIP3bpqsElNEYlfmPT1JAUaL9Oast0599lk3I2xJb8O11aD8cwnI2nm8ouG+A2t8 Xxwg== X-Gm-Message-State: AODbwcBvj8PmBiqKiXqYqDEBpNg9TlWIMwV9KD//6F2MRtc5czZj8h/p 3VSTDXq+Nw9D0MK/gAB/xtMky4wqTw== X-Received: by 10.159.54.132 with SMTP id p4mr1210996uap.31.1494791081814; Sun, 14 May 2017 12:44:41 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.133.5 with HTTP; Sun, 14 May 2017 12:44:21 -0700 (PDT) In-Reply-To: References: <6D5827E3-C1D9-4097-88B0-7EE210239602@chalmers.se> From: Bas Spitters Date: Sun, 14 May 2017 21:44:21 +0200 Message-ID: Subject: Re: [HoTT] cubical stacks To: Michael Shulman Cc: Thierry Coquand , homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c04108271f2a6054f812b4f" --94eb2c04108271f2a6054f812b4f Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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 > 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 w= as > > 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=C3=A9drot and Nicolas Tab= areau, > > but for cubical type theory). > > > > Given a family of types F(c), non necessarily fibrant, over a base typ= e > > Cov, > > we associate the family of (definitional) monads D_c (X) =3D 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 Grou= ps > > "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. > --94eb2c04108271f2a6054f812b4f Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks Mike. This is very informative.

I= s your oo-exact completion related to the homotopy exact completion by Benn= o and Ieke?
https://arxiv.o= rg/abs/1603.02456

On Sun, May 14, 2017 at 11:53 AM, Michael Shulman <shu..= .@sandiego.edu> wrote:
This= is very nice.=C2=A0 I have two questions/comments:

1. I would not expect the "stack" model to inherit inductive type= s
like coproducts, natural numbers objects, W-types, and HITs with
judgmental computation rules.=C2=A0 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.=C2=A0 Is that right?

2. I agree that the word "stack" is appropriate for the internal<= br> construction, which is a categorification of Lawvere-Tierney sheaves,
for which the word "sheaf" is often used.=C2=A0 However, when per= formed
inside the "cubical presheaves on a space" model, I don't bel= ieve it
produces oo-stacks in the usual sense of the external set theory,
because "cubical presheaves on a space" with this sort of "p= ointwise
homotopy theory" don't present the homotopy theory of oo-presheave= s on
that space, at least not without some extra fibrancy condition.=C2=A0 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> wr= ote:
>=C2=A0 In this message, I would like to present quickly a generalisatio= n
> 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.
>
>=C2=A0 =C2=A0The 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=C3=A9drot and Nicolas Ta= bareau,
> but for cubical type theory).
>
>=C2=A0 Given a family of types F(c), non necessarily fibrant, over a ba= se type
> Cov,
> we associate the family of (definitional) monads=C2=A0 D_c (X) =3D X^{= F(c)} with
> unit maps m_c : X -> D_c(X).
>=C2=A0 =C2=A0We say that Cov,F=C2=A0 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 t= ype of
> descent
> data for X for the covering c.
>=C2=A0 =C2=A0We 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.
>=C2=A0 The following note contains a summary of these discussions, with= an example
> of
> a covering family Cov,F.
>
>=C2=A0 Thierry
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an
> email to Homot= opyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/opto= ut.

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

--94eb2c04108271f2a6054f812b4f--