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