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

> 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

> >

> >

>= ; >

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

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

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