From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 6 Jun 2017 03:03:29 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Cc: awo...@cmu.edu, shu...@sandiego.edu, Thierry...@cse.gu.se, homotopyt...@googlegroups.com Message-Id: <1c2cb641-89e3-444d-aa0c-cb8ccb79cf3c@googlegroups.com> In-Reply-To: <2efaa818-9ed1-459f-a3a5-a274d19e6a96@googlegroups.com> References: <1128BE39-BBC4-4DC6-8792-20134A6CAECD@chalmers.se> <292DED31-6CB3-49A1-9128-5AFD04B9C2F2@cmu.edu> <9F58F820-A54A-46E7-93DC-F814D4BEE0C6@cmu.edu> <2efaa818-9ed1-459f-a3a5-a274d19e6a96@googlegroups.com> Subject: Re: [HoTT] Semantics of higher inductive types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2050_632979915.1496743409515" ------=_Part_2050_632979915.1496743409515 Content-Type: multipart/alternative; boundary="----=_Part_2051_1423789231.1496743409515" ------=_Part_2051_1423789231.1496743409515 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Actually, I've just noticed that doesn't quite work - I want to say that a= =20 map is a weak fibration if it has a (uniform choice of) diagonal fillers=20 for lifting problems against generating cofibrations where the bottom map= =20 factors through the projection I x V -> V, but that doesn't seem to be=20 cofibrantly generated. Maybe it's still possible to do something like=20 fibrant replacement anyway. Andrew On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote: > > I've been thinking a bit about abstract ways of looking at the HITs in=20 > cubical type theory, and I don't have a complete proof, but I think=20 > actually the same sort of thing should work for simplicial sets. > > We already know that the fibrations in the usual model structure on=20 > simplicial sets can be defined as maps with the rlp against the pushout= =20 > product of generating cofibrations with interval endpoint inclusions (in= =20 > Christian's new paper on model=20 > structures he cites for this result Chapter IV, section 2 of P. Gabriel a= nd=20 > M. Zisman. Calculus of fractions and homotopy theory, but I'm not familia= r=20 > with the proof myself). > > Now a generating trivial cofibration is the pushout product of a=20 > generating cofibration with endpoint inclusion, so its codomain is of the= =20 > form I x V, where V is the codomain of the generating cofibration (which= =20 > for cubical sets and simplicial sets is representable). Then we get anoth= er=20 > map by composing with projection I x V -> V, which is a retract of the=20 > generating trivial cofibration and so also a trivial cofibration. If a ma= p=20 > has the rlp against all such maps, then call it a weak fibration. Then I= =20 > think the resulting awfs of "weak fibrant replacement" should be stable= =20 > under pullback (although of course, the right maps in the factorisation a= re=20 > only weak fibrations, not fibrations in general). > > Then eg for propositional truncation, construct the "fibrant truncation"= =20 > monad by the coproduct of truncation monad with weak fibrant replacement.= =20 > In general, given a map X -> Y, the map ||X|| -> Y will only be a weak=20 > fibration, but if X -> Y is fibration then I think the map ||X|| -> Y=20 > should be also. I think the way to formulate this would be as a=20 > distributive law - the fibrant replacement monad distributes over the=20 > (truncation + weak fibrant replacement) monad. It looks to me like the sa= me=20 > thing that works in cubical sets should also work here - first define a= =20 > "box flattening" operation for any fibration (i.e. the operation labelled= =20 > as "forward" in Thierry's note), then show that this operation lifts=20 > through the HIT constructors to give a box flattening operation on the HI= T,=20 > then show that in general weak fibration plus box flattening implies=20 > fibration, (Maybe one way to do this would be to note that the cubical se= t=20 > argument is mostly done internally in cubical type theory, and simplicial= =20 > sets model cubical type theory by Orton & Pitts, Axioms for Modelling=20 > Cubical Type Theory in a Topos=20 > > ) > > Best, > Andrew > > > > On Thursday, 1 June 2017 18:08:58 UTC+2, Peter LeFanu Lumsdaine wrote: >> >> On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey wrote: >> > >> > you mean the propositional truncation or suspension operations might= =20 >> 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=20 >> with the construction of Mike=E2=80=99s and my paper, they do. And addi= ng stronger=20 >> conditions on the cardinal used won=E2=80=99t help. The problem is that= one takes=20 >> a fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80=9D to= the suspension=20 >> (more precisely: a (TC,F) factorisation, to go from the universal family= of=20 >> pre-suspensions to the universal family of suspensions); and fibrant=20 >> replacement blows up the fibers to be the size of the *base* of the=20 >> family. So the pre-suspension is small, but the suspension =E2=80=94 al= though=20 >> 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,=20 >> together with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B over =CE= =A3, and a homotopy m from=20 >> N to S over =CE=A3, which together exhibit U as =E2=80=9Cclosed under su= spension=E2=80=9D. >> >> I asked a related question on mathoverflow a couple of years ago:=20 >> https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibre= wise-suspension-of-fibrations-in-simplicial-sets=20 >> David White suggested he could see an answer to that question (which wo= uld=20 >> probably also answer (*) here) based on the comments by Karol Szumi=C5= =82o and=20 >> Tyler Lawson, using the adjunction with Top, but I wasn=E2=80=99t quite = able to=20 >> piece it together. >> >> =E2=80=93p. >> =20 >> > >> > > On Jun 1, 2017, at 11:38 AM, Michael Shulman = =20 >> wrote: >> > > >> > > Do we actually know that the Kan simplicial set model has a *univers= e >> > > 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 t= he >> > > 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 implicatio= ns >> > > 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= =20 >> HITs, >> > >> the paper >> > >> on cubical type theory describes a way to interpret HIT together= =20 >> with a >> > >> univalent >> > >> universe which is stable by HIT operations. This gives in particula= r=20 >> 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 hav= e lots of nice=20 >> properties >> > >> for models of HoTT >> > >> =E2=80=94 but there was never really a question of the consistency = or=20 >> coherence of >> > >> simple HITs like propositional truncation or suspension. >> > >> >> > >> the advance in the L-S paper is to give a general scheme for=20 >> 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=20 >> 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. Bu= t=20 >> it can >> > >> directly >> > >> be transformed to a semantical interpretation, as explained in the= =20 >> 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=20 >> explicit in >> > >> the note >> > >> what is the problem solved by the =E2=80=9Cflattening boxes=E2=80= =9D method. >> > >> >> > >> Only the cases of the spheres and propositional truncation are=20 >> described, >> > >> but one >> > >> would expect the method to generalise to other HITs covered e.g. in= =20 >> the HoTT >> > >> book. >> > >> >> > >> On 25 May 2017, at 20:25, Michael Shulman =20 >> 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-behav= ed >> > >> 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 specifi= c >> > >> 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= =20 >> as >> > >> simplicial sets) and any locally presentable locally cartesian clos= ed >> > >> 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= our >> > >> results apply. >> > >> >> > >> -- >> > >> You received this message because you are subscribed to the Google= =20 >> Groups >> > >> "Homotopy Type Theory" group. >> > >> To unsubscribe from this group and stop receiving emails from it,= =20 >> 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= =20 >> Groups >> > >> "Homotopy Type Theory" group. >> > >> To unsubscribe from this group and stop receiving emails from it,= =20 >> 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= =20 >> Groups >> > >> "Homotopy Type Theory" group. >> > >> To unsubscribe from this group and stop receiving emails from it,= =20 >> 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= =20 >> Groups "Homotopy Type Theory" group. >> > > To unsubscribe from this group and stop receiving emails from it,=20 >> 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=20 >> Groups "Homotopy Type Theory" group. >> > To unsubscribe from this group and stop receiving emails from it, send= =20 >> an email to HomotopyTypeThe...@googlegroups.com. >> > For more options, visit https://groups.google.com/d/optout. >> > ------=_Part_2051_1423789231.1496743409515 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Actually, I've just noticed that doesn't quite wor= k - I want to say that a map is a weak fibration if it has a (uniform choic= e of) diagonal fillers for lifting problems against generating cofibrations= where the bottom map factors through the projection I x V -> V, but tha= t doesn't seem to be cofibrantly generated. Maybe it's still possib= le to do something like fibrant replacement anyway.

Andr= ew

On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:
I've been = thinking a bit about abstract ways of looking at the HITs in cubical type t= heory, and I don't have a complete proof, but I think actually the same= sort of thing should work for simplicial sets.

We alrea= dy know that the fibrations in the usual model structure on simplicial sets= can be defined as maps with the rlp against the pushout product of generat= ing cofibrations with interval endpoint inclusions (in Christian's new = paper on model structures he cites for this= result Chapter IV, section 2 of P. Gabriel and M. Zisman. Calculus of frac= tions and homotopy theory, but I'm not familiar with the proof myself).=

Now a generating trivial cofibration is the pusho= ut product of a generating cofibration with endpoint inclusion, so its codo= main is of the form I x V, where V is the codomain of the generating cofibr= ation (which for cubical sets and simplicial sets is representable). Then w= e get another map by composing with projection I x V -> V, which is a re= tract of the generating trivial cofibration and so also a trivial cofibrati= on. If a map has the rlp against all such maps, then call it a weak fibrati= on. Then I think the resulting awfs of "weak fibrant replacement"= should be stable under pullback (although of course, the right maps in the= factorisation are only weak fibrations, not fibrations in general).
<= div>
Then eg for propositional truncation, construct the &quo= t;fibrant truncation" monad by the coproduct of truncation monad with = weak fibrant replacement. In general, given a map X -> Y, the map ||X|| = -> Y will only be a weak fibration, but if X -> Y is fibration then I= think the map ||X|| -> Y should be also. I think the way to formulate t= his would be as a distributive law - the fibrant replacement monad distribu= tes over the (truncation + weak fibrant replacement) monad. It looks to me = like the same thing that works in cubical sets should also work here - firs= t define a "box flattening" operation for any fibration (i.e. the= operation labelled as "forward" in Thierry's note), then sho= w that this operation lifts through the HIT constructors to give a box flat= tening operation on the HIT, then show that in general weak fibration plus = box flattening implies fibration, (Maybe one way to do this would be to not= e that the cubical set argument is mostly done internally in cubical type t= heory, and simplicial sets model cubical type theory by Orton & Pitts,= =C2=A0Axioms for Modelling Cubical Type = Theory in a Topos)

Best,
Andrew



On Thursday, 1 June 2017 18:08:58= UTC+2, Peter LeFanu Lumsdaine wrote:
On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
> you mean the pr= opositional truncation or suspension operations might lead to cardinals out= side of a Grothendieck Universe?

Exactly, yes.=C2=A0 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.=C2=A0 And adding stronger conditions = on the cardinal used won=E2=80=99t help.=C2=A0 The problem is that one take= s 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 univ= ersal family of pre-suspensions to the universal family of suspensions); an= d fibrant replacement blows up the fibers to be the size of the *base* of t= he family.=C2=A0 So the pre-suspension is small, but the suspension =E2=80= =94 although essentially small =E2=80=94 ends up as large as the universe o= ne=E2=80=99s using.

So here=E2=80=99s a very precise problem which i= s 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 approp= riate 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= suspension=E2=80=9D.

I asked a related question on mathoverflow a c= ouple 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 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 able to piece it together.

=E2=80=93p.
=C2=A0
><= br>> > On Jun 1, 2017, at 11:38 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> >
> > Do we a= ctually know that the Kan simplicial set model has a *universe
> >= closed under* even simple HITs?=C2=A0 It's not trivial because this wo= uld
> > mean we could (say) propositionally truncate or suspend th= e generic
> > small Kan fibration and get another *small* Kan fibr= ation, 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
> > s= cheme, only a general semantic framework with suggestive implications
&g= t; > for the corresponding syntax.)
> >
> >
> &g= t;
> > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey <awo...@cmu.edu> wrote:
> >>
> >> O= n Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thier..= .@cse.gu.se>
> >> wrote:
> >>
> >&g= t; =C2=A0If we are only interested in providing one -particular- model of H= ITs,
> >> the paper
> >> on =C2=A0cubical type =C2= =A0theory describes a way to =C2=A0interpret HIT together with a
> &g= t;> univalent
> >> universe which is stable by HIT operation= s. This gives in particular the
> >> consistency
> >&g= t; 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 w= rong =E2=80=94 I love the cubes, and they have lots of nice properties
&= gt; >> for models of HoTT
> >> =E2=80=94 but there was ne= ver really a question of the consistency or coherence of
> >> s= imple HITs like propositional truncation or suspension.
> >>> >> the advance in the L-S paper is to give a general scheme for= defining HITs
> >> syntactically
> >> (a definitio= n, 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.
&g= t; >>
> >> Steve
> >>
> >>
>= ; >> =C2=A0The approach uses an operation of =C2=A0=E2=80=9Cflattenin= g an open box=E2=80=9D, which solves
> >> in
> >> t= his 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, =C2=A0we
> >> limited
> >>= ourselves =C2=A0to a syntactical presentation of this interpretation. But = it can
> >> directly
> >> be transformed to a seman= tical interpretation, as explained in the following
> >> note> >> (which also incorporates a nice simplification of the opera= tion of
> >> flattering
> >> an open box noticed by= my coauthors). I also try to make more explicit in
> >> the no= te
> >> what is the problem solved by the =E2=80=9Cflattening b= oxes=E2=80=9D method.
> >>
> >> Only the cases of t= he spheres and propositional truncation are described,
> >> but= one
> >> would expect the method to generalise to other HITs c= overed e.g. in the HoTT
> >> book.
> >>
> >= ;> On 25 May 2017, at 20:25, Michael Shulman <shu= ...@sandiego.edu> wrote:
> >>
> >> The follo= wing long-awaited paper is now available:
> >>
> >>= Semantics of higher inductive types
> >> Peter LeFanu Lumsdain= e, Mike Shulman
> >> https://arxiv.org/abs/1705= .07088
> >>
> >> From the abstract:
>= ; >>
> >> We introduce the notion of *cell monad with par= ameters*: a
> >> semantically-defined scheme for specifying hom= otopically 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. Whe= n 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 localisati= ons.
> >>
> >> Our results apply in any sufficientl= y nice Quillen model category,
> >> including any right proper = simplicial Cisinski model category (such as
> >> simplicial set= s) and any locally presentable locally cartesian closed
> >> ca= tegory (such as sets) with its trivial model structure. In
> >>= particular, any locally presentable locally cartesian closed
> >&= gt; (=E2=88=9E,1)-category is presented by some model category to which our=
> >> results apply.
> >>
> >> --
&g= t; >> You received this message because you are subscribed to the Goo= gle Groups
> >> "Homotopy Type Theory" group.
>= >> To unsubscribe from this group and stop receiving emails from it,= send an
> >> email to HomotopyTypeTheory+<= wbr>unsub...@googlegroups.com.
> >> For more options, visit= https://groups.google.com/d/optout.
&= gt; >>
> >>
> >>
> >> --
> = >> You received this message because you are subscribed to the Google= Groups
> >> "Homotopy Type Theory" group.
> &g= t;> To unsubscribe from this group and stop receiving emails from it, se= nd an
> >> email to HomotopyTypeTheory+unsub...@googlegroups.com.
> >> For more options, visit https://groups.google.com/d/optout.
>= >>
> >>
> >> --
> >> You receive= d this message because you are subscribed to the Google Groups
> >= > "Homotopy Type Theory" group.
> >> To unsubscrib= e from this group and stop receiving emails from it, send an
> >&g= t; email to HomotopyTypeTheory+unsub...@googlegrou= ps.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 unsub= scribe from this group and stop receiving emails from it, send an email to = HomotopyTypeTheory+unsub...@googlegroups.com.<= br>> > For more options, visit https://group= s.google.com/d/optout.
>
> --
> You received thi= s message because you are subscribed to the Google Groups "Homotopy Ty= pe Theory" group.
> To unsubscribe from this group and stop rece= iving emails from it, send an email to HomotopyTypeTheo= ry+unsub...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
------=_Part_2051_1423789231.1496743409515-- ------=_Part_2050_632979915.1496743409515--