From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.57.65 with SMTP id l59mr984450qte.74.1496333338671; Thu, 01 Jun 2017 09:08:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.11.196 with SMTP id 62ls6062274oth.36.gmail; Thu, 01 Jun 2017 09:08:58 -0700 (PDT) X-Received: by 10.200.54.197 with SMTP id b5mr987947qtc.11.1496333337941; Thu, 01 Jun 2017 09:08:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1496333337; cv=none; d=google.com; s=arc-20160816; b=x+d3eWEyYstGIwyuBJpj3AZ4JFXjAIGOJOL10POUN2W8GaWncuGENOF7PsGfictT8x K3IYdBZOGJZlKoamHhRFyjS1XIlkPKOczAV+wrFUCsRTRko2fZ+ABDBmy2UxkZhjlG1R /1+DWWpJ9MnoHMShohFvjEriRp77cYkf4i/CBt72jOgjF/ewuVL6Ff327emx6fzKzROW /rpVmrFCKKyGbZXWMLqZizLVLFlUZm7Ff+4GqHTZzEcu0mZ3PLTFFNPKxDAbjRO+psfz lEhunrVZyRmRU6ZXgo4Xu4WvJ88ck37UnDOzH3RczrmB34Twwwx5KJke1UgxU7cqACR6 BwIQ== 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=qr/zDPIGHwIWF0MhxX18+1hSBV2EZ4RDOcFY5E/as2c=; b=PP7sQqj2tmzQBaFf0VwrsP++LZef7iUPQgKgDIMW0eAmmMTKSNZ4mcCfZxspHuqJyh V2rg5VV7IfvGb1uvq7EIqLHpP0RYnyyeEyrR2HUWviv4LB1qTlNJYbgRwxoOsU8STkBI LrXz57R9z9KGK0xd5C7DtRX3G5pHML+GokZL/rWZcLCdBvDv/LxIz4boufB3XSlAOUGJ malBsc5jlKC71Um8EjXvVLaRDVVbr+/7zOrN5RlYm0mZf9nlSqBQpHofKNQnnCjWFFa9 fbzHT66AP+6FAJm24WHKpHKTErGLIkxttU38nIr2IFceaAiSkRoCg/L4Lo2L1zfUdnG2 rlpw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::234 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x234.google.com (mail-ua0-x234.google.com. [2607:f8b0:400c:c08::234]) by gmr-mx.google.com with ESMTPS id n204si645230vkd.7.2017.06.01.09.08.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 01 Jun 2017 09:08:57 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::234 as permitted sender) client-ip=2607:f8b0:400c:c08::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::234 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x234.google.com with SMTP id y4so30240935uay.2 for ; Thu, 01 Jun 2017 09:08:57 -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=qr/zDPIGHwIWF0MhxX18+1hSBV2EZ4RDOcFY5E/as2c=; b=d07+IwHPeapM5Olct+2W4sOS1b6+/HM4PZI32QgyH9qGL2YA/blD4z5lkNwCBBhrR+ Brj1Fki+4smUTqu8dqA4+RWIFGTYI8k48ZwtOUF4tRQQVzGuThvJvlG9+NQlMatySYRp 6hZv6UPsfnKIPCcXjo79QN6lnX2yC3S5AdMMy0B6DPG50FxAOY5jVoqAcfBSc6vv9crb XeCAzRvIXcAUIj/jVVxwkeEoZx+M2jS3Ax4kWghg3wuhcZDj4jNLvzm3lnyAnyRxaL6y 8hO1Vb6zfcgSla3M8hP2ph5aGxtuzwfPFzAkFtnRGiSldi73kvM1IHOZ6mk+F+zRmYAo h9Tg== X-Gm-Message-State: AODbwcBjD8xCmmuhojUe4ZvOvQCEvqrG5jPPXO1JW2s3mkc892f26OSE OShoqxM8lUtMpGzbUrUDWQ0HHBCh/pGy X-Received: by 10.176.64.103 with SMTP id h94mr1199869uad.18.1496333337639; Thu, 01 Jun 2017 09:08:57 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.7.217 with HTTP; Thu, 1 Jun 2017 09:08:57 -0700 (PDT) In-Reply-To: <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> From: Peter LeFanu Lumsdaine Date: Thu, 1 Jun 2017 19:08:57 +0300 Message-ID: Subject: Re: [HoTT] Semantics of higher inductive types To: Steve Awodey Cc: Michael Shulman , Thierry Coquand , homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c0433460e72ba0550e841da" --94eb2c0433460e72ba0550e841da Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey wrote: > > you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe? Exactly, yes. There=E2=80=99s no reason I know of to think they *need* to,= but with the construction of Mike=E2=80=99s and my paper, they do. And adding = stronger conditions on the cardinal used won=E2=80=99t help. The problem is that on= e takes a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D to th= e suspension (more precisely: a (TC,F) factorisation, to go from the universal family of pre-suspensions to the universal family of suspensions); and fibrant replacement blows up the fibers to be the size of the *base* of the family. So the pre-suspension is small, but the suspension =E2=80=94 altho= ugh essentially small =E2=80=94 ends up as large as the universe one=E2=80=99s = using. So here=E2=80=99s a very precise problem which is as far as I know open: (*) Construct an operation =CE=A3 : U =E2=80=93> U, where U is Voevodsky=E2= =80=99s universe, together with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B over =CE=A3,= and a homotopy m from N to S over =CE=A3, which together exhibit U as =E2=80=9Cclosed under suspe= nsion=E2=80=9D. I asked a related question on mathoverflow a couple of years ago: https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibrewis= e-suspension-of-fibrations-in-simplicial-sets David White suggested he could see an answer to that question (which would probably also answer (*) here) based on the comments by Karol Szumi=C5=82o = and Tyler Lawson, using the adjunction with Top, but I wasn=E2=80=99t quite abl= e to piece it together. =E2=80=93p. > > > On Jun 1, 2017, at 11:38 AM, Michael Shulman wrote: > > > > Do we actually know that the Kan simplicial set model has a *universe > > closed under* even simple HITs? It's not trivial because this would > > mean we could (say) propositionally truncate or suspend the generic > > small Kan fibration and get another *small* Kan fibration, whereas the > > base of these fibrations is not small, and fibrant replacement doesn't > > in general preserve smallness of fibrations with large base spaces. > > > > (Also, the current L-S paper doesn't quite give a general syntactic > > scheme, only a general semantic framework with suggestive implications > > for the corresponding syntax.) > > > > > > > > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey wrote: > >> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand > >> wrote: > >> > >> If we are only interested in providing one -particular- model of HITs= , > >> the paper > >> on cubical type theory describes a way to interpret HIT together with a > >> univalent > >> universe which is stable by HIT operations. This gives in particular the > >> consistency > >> and the proof theoretic power of this extension of type theory. > >> > >> > >> but the Kan simplicial set model already does this =E2=80=94 right? > >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes, and they have l= ots of nice properties > >> for models of HoTT > >> =E2=80=94 but there was never really a question of the consistency or coherence of > >> simple HITs like propositional truncation or suspension. > >> > >> the advance in the L-S paper is to give a general scheme for defining HITs > >> syntactically > >> (a definition, if you like, of what a HIT is, rather than a family of > >> examples), > >> and then a general description of the semantics of these, > >> in a range of models of the basic theory. > >> > >> Steve > >> > >> > >> The approach uses an operation of =E2=80=9Cflattening an open box=E2= =80=9D, which solves > >> in > >> this case the issue of interpreting HIT with parameters (such as > >> propositional > >> truncation or suspension) without any coherence issue. > >> Since the syntax used in this paper is so close to the semantics, we > >> limited > >> ourselves to a syntactical presentation of this interpretation. But it can > >> directly > >> be transformed to a semantical interpretation, as explained in the following > >> note > >> (which also incorporates a nice simplification of the operation of > >> flattering > >> an open box noticed by my coauthors). I also try to make more explicit in > >> the note > >> what is the problem solved by the =E2=80=9Cflattening boxes=E2=80=9D m= ethod. > >> > >> Only the cases of the spheres and propositional truncation are described, > >> but one > >> would expect the method to generalise to other HITs covered e.g. in the HoTT > >> book. > >> > >> On 25 May 2017, at 20:25, Michael Shulman wrote: > >> > >> The following long-awaited paper is now available: > >> > >> Semantics of higher inductive types > >> Peter LeFanu Lumsdaine, Mike Shulman > >> https://arxiv.org/abs/1705.07088 > >> > >> From the abstract: > >> > >> We introduce the notion of *cell monad with parameters*: a > >> semantically-defined scheme for specifying homotopically well-behaved > >> notions of structure. We then show that any suitable model category > >> has *weakly stable typal initial algebras* for any cell monad with > >> parameters. When combined with the local universes construction to > >> obtain strict stability, this specializes to give models of specific > >> higher inductive types, including spheres, the torus, pushout types, > >> truncations, the James construction, and general localisations. > >> > >> Our results apply in any sufficiently nice Quillen model category, > >> including any right proper simplicial Cisinski model category (such as > >> simplicial sets) and any locally presentable locally cartesian closed > >> category (such as sets) with its trivial model structure. In > >> particular, any locally presentable locally cartesian closed > >> (=E2=88=9E,1)-category is presented by some model category to which ou= r > >> results apply. > >> > >> -- > >> 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. > >> > >> > >> -- > >> 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. > > -- > 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. --94eb2c0433460e72ba0550e841da Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
> yo= u mean the propositional truncation or suspension operations might lead to = cardinals outside of a Grothendieck Universe?

Exactly, yes.=C2=A0 Th= ere=E2=80=99s no reason I know of to think they *need* to, but with the con= struction of Mike=E2=80=99s and my paper, they do.=C2=A0 And adding stronge= r conditions on the cardinal used won=E2=80=99t help.=C2=A0 The problem is = that one takes a fibrant replacement to go from the =E2=80=9Cpre-suspension= =E2=80=9D to the suspension (more precisely: a (TC,F) factorisation, to go = from the universal family of pre-suspensions to the universal family of sus= pensions); and fibrant replacement blows up the fibers to be the size of th= e *base* of the family.=C2=A0 So the pre-suspension is small, but the suspe= nsion =E2=80=94 although essentially small =E2=80=94 ends up as large as th= e universe one=E2=80=99s using.

So here=E2=80=99s a very precise pro= blem which is as far as I know open:

(*) Construct an operation =CE= =A3 : U =E2=80=93> U, where U is Voevodsky=E2=80=99s universe, together = with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B over =CE=A3, and a= homotopy m from N to S over =CE=A3, which together exhibit U as =E2=80=9Cc= losed under suspension=E2=80=9D.

I asked a related question on matho= verflow a couple of years ago: https://mathoverflow.net/questions/219588/pullback-stable-mod= el-of-fibrewise-suspension-of-fibrations-in-simplicial-sets =C2=A0David= White suggested he could see an answer to that question (which would proba= bly also answer (*) here) based on the comments by Karol Szumi=C5=82o and T= yler Lawson, using the adjunction with Top, but I wasn=E2=80=99t quite able= to piece it together.

=E2=80=93p.
=C2=A0
>
> > On= Jun 1, 2017, at 11:38 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> >
> > Do = we actually know that the Kan simplicial set model has a *universe
> = > closed under* even simple HITs?=C2=A0 It's not trivial because thi= s would
> > mean we could (say) propositionally truncate or suspen= d the generic
> > small Kan fibration and get another *small* Kan = fibration, whereas the
> > base of these fibrations is not small, = and fibrant replacement doesn't
> > in general preserve smalln= ess of fibrations with large base spaces.
> >
> > (Also, = the current L-S paper doesn't quite give a general syntactic
> &g= t; scheme, only a general semantic framework with suggestive implications> > for the corresponding syntax.)
> >
> >
>= ; >
> > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey <awo...@cmu.edu> wrote:
> >><= br>> >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thierry...@cse.gu.se>
> >&= gt; wrote:
> >>
> >> =C2=A0If we are only intereste= d in providing one -particular- model of HITs,
> >> the paper> >> on =C2=A0cubical type =C2=A0theory describes a way to =C2= =A0interpret HIT together with a
> >> univalent
> >>= ; universe which is stable by HIT operations. This gives in particular the<= br>> >> consistency
> >> and the proof theoretic power= of this extension of type theory.
> >>
> >>
>= ; >> but the Kan simplicial set model already does this =E2=80=94 rig= ht?
> >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes,= and they have lots of nice properties
> >> for models of HoTT<= br>> >> =E2=80=94 but there was never really a question of the con= sistency or coherence of
> >> simple HITs like propositional tr= uncation or suspension.
> >>
> >> the advance in th= e L-S paper is to give a general scheme for defining HITs
> >> = syntactically
> >> (a definition, if you like, of what a HIT is= , rather than a family of
> >> examples),
> >> and = then a general description of the semantics of these,
> >> in a= range of models of the basic theory.
> >>
> >> Ste= ve
> >>
> >>
> >> =C2=A0The approach us= es an operation of =C2=A0=E2=80=9Cflattening an open box=E2=80=9D, which so= lves
> >> in
> >> this case the issue of interpreti= ng HIT with parameters (such as
> >> propositional
> >= > truncation or suspension) without any coherence issue.
> >>= ; Since the syntax used in this paper is so close to the semantics, =C2=A0w= e
> >> limited
> >> ourselves =C2=A0to a syntactica= l presentation of this interpretation. But it can
> >> directly=
> >> be transformed to a semantical interpretation, as explain= ed in the following
> >> note
> >> (which also inco= rporates a nice simplification of the operation of
> >> flatter= ing
> >> an open box noticed by my coauthors). I also try to ma= ke more explicit in
> >> the note
> >> what is the = problem solved by the =E2=80=9Cflattening boxes=E2=80=9D method.
> &g= t;>
> >> Only the cases of the spheres and propositional tru= ncation are described,
> >> but one
> >> would expe= ct the method to generalise to other HITs covered e.g. in the HoTT
> = >> book.
> >>
> >> On 25 May 2017, at 20:25, = Michael Shulman <shu...@sandiego.= edu> wrote:
> >>
> >> The following long-awa= ited paper is now available:
> >>
> >> Semantics of= higher inductive types
> >> Peter LeFanu Lumsdaine, Mike Shulm= an
> >> https://ar= xiv.org/abs/1705.07088
> >>
> >> From the abstr= act:
> >>
> >> We introduce the notion of *cell mon= ad with parameters*: a
> >> semantically-defined scheme for spe= cifying homotopically well-behaved
> >> notions of structure. W= e then show that any suitable model category
> >> has *weakly s= table typal initial algebras* for any cell monad with
> >> para= meters. When combined with the local universes construction to
> >= > obtain strict stability, this specializes to give models of specific> >> higher inductive types, including spheres, the torus, pusho= ut types,
> >> truncations, the James construction, and general= localisations.
> >>
> >> Our results apply in any = sufficiently nice Quillen model category,
> >> including any ri= ght proper simplicial Cisinski model category (such as
> >> sim= plicial sets) and any locally presentable locally cartesian closed
> = >> category (such as sets) with its trivial model structure. In
&g= t; >> particular, any locally presentable locally cartesian closed> >> (=E2=88=9E,1)-category is presented by some model category t= o which our
> >> results apply.
> >>
> >&g= t; --
> >> You received this message because you are subscribed= to the Google Groups
> >> "Homotopy Type Theory" gro= up.
> >> To unsubscribe from this group and stop receiving emai= ls from it, send an
> >> email to HomotopyTypeThe...@googlegroups.com.
>= >> For more options, visit https://groups.google.com/d/optout.
> >>
> >= >
> >>
> >> --
> >> You received thi= s message because you are subscribed to the Google Groups
> >> = "Homotopy Type Theory" group.
> >> To unsubscribe fro= m this group and stop receiving emails from it, send an
> >> em= ail to HomotopyType= The...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optou= t.
> >>
> >>
> >> --
> >&g= t; You received this message because you are subscribed to the Google Group= s
> >> "Homotopy Type Theory" group.
> >>= To unsubscribe from this group and stop receiving emails from it, send an<= br>> >> email to HomotopyTypeThe...@googlegroups.com.
> >> For more o= ptions, visit https://groups= .google.com/d/optout.
> >
> > --
> > You rec= eived this message because you are subscribed to the Google Groups "Ho= motopy Type Theory" group.
> > To unsubscribe from this group= and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.<= br>> > 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 gr= oup and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit
https://groups.google.com/d/optout.
--94eb2c0433460e72ba0550e841da--