From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 6 Jun 2017 13:59:11 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Cc: wakeli...@gmail.com, awo...@cmu.edu, Thierry...@cse.gu.se Message-Id: In-Reply-To: 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> <1c2cb641-89e3-444d-aa0c-cb8ccb79cf3c@googlegroups.com> Subject: Re: [HoTT] Semantics of higher inductive types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1919_1893536486.1496782751457" ------=_Part_1919_1893536486.1496782751457 Content-Type: multipart/alternative; boundary="----=_Part_1920_891118772.1496782751459" ------=_Part_1920_891118772.1496782751459 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I don't have a clear idea - the only examples I know of are simplicial=20 sets, variants of cubical sets and the effective topos. Also I don't know= =20 which HITs can be done with this kind of approach. On Tuesday, 6 June 2017 21:36:56 UTC+2, Michael Shulman wrote: > > What class of homotopy theories can be presented by such models?=20 > > On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan > wrote:=20 > > I don't know how general this is exactly in practice, but I think it=20 > should=20 > > work in the setting that appears in van de Berg, Frumin A=20 > homotopy-theoretic=20 > > model of function extensionality in the effective topos, which=20 > regardless of=20 > > the title is not just the effective topos, but any topos together with = a=20 > > interval object with connections, a dominance satisfying certain=20 > conditions,=20 > > with fibrations defined as maps with the rlp against pushout product of= =20 > > endpoint inclusions and elements of the dominance (& in addition there= =20 > > should be some more conditions to ensure that free monads on pointed=20 > > endofunctors exist).=20 > >=20 > >=20 > > I'm a bit more confident that it works now. The class of weak fibration= s=20 > is=20 > > not cofibrantly generated in the usual sense (as I claimed in the first= =20 > > post), but they are in the more general sense by Christian Sattler in= =20 > > section 6 of The Equivalence Extension Property and Model Structures.= =20 > Then a=20 > > version of step 1 of the small object argument applies to Christian's= =20 > > definition, which gives a pointed endofunctor whose algebras are the=20 > weak=20 > > fibrations. The same technique can also be used to describe "box=20 > flattening"=20 > > (which should probably be called something else, like "cylinder=20 > flattening"=20 > > in the general setting).=20 > >=20 > >=20 > > Andrew=20 > >=20 > > On Tuesday, 6 June 2017 15:35:36 UTC+2, Michael Shulman wrote:=20 > >>=20 > >> I'll be interested to see if you can make it work!=20 > >>=20 > >> But I'd be much more interested if there is something that can be done= =20 > >> in a general class of models, rather than a particular one like=20 > >> cubical or simplicial sets.=20 > >>=20 > >> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan =20 > wrote:=20 > >> > Actually, I've just noticed that doesn't quite work - I want to say= =20 > that=20 > >> > a=20 > >> > map is a weak fibration if it has a (uniform choice of) diagonal=20 > fillers=20 > >> > for=20 > >> > lifting problems against generating cofibrations where the bottom ma= p=20 > >> > factors through the projection I x V -> V, but that doesn't seem to= =20 > be=20 > >> > cofibrantly generated. Maybe it's still possible to do something lik= e=20 > >> > fibrant replacement anyway.=20 > >> >=20 > >> > Andrew=20 > >> >=20 > >> >=20 > >> > On Tuesday, 6 June 2017 11:19:37 UTC+2, Andrew Swan wrote:=20 > >> >>=20 > >> >> I've been thinking a bit about abstract ways of looking at the HITs= =20 > in=20 > >> >> cubical type theory, and I don't have a complete proof, but I think= =20 > >> >> actually=20 > >> >> the same sort of thing should work for simplicial sets.=20 > >> >>=20 > >> >> 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=20 > pushout=20 > >> >> product of generating cofibrations with interval endpoint inclusion= s=20 > >> >> (in=20 > >> >> Christian's new paper on model structures he cites for this result= =20 > >> >> Chapter=20 > >> >> IV, section 2 of P. Gabriel and M. Zisman. Calculus of fractions an= d=20 > >> >> homotopy theory, but I'm not familiar with the proof myself).=20 > >> >>=20 > >> >> Now a generating trivial cofibration is the pushout product of a=20 > >> >> generating cofibration with endpoint inclusion, so its codomain is= =20 > of=20 > >> >> the=20 > >> >> form I x V, where V is the codomain of the generating cofibration= =20 > >> >> (which for=20 > >> >> cubical sets and simplicial sets is representable). Then we get=20 > another=20 > >> >> map=20 > >> >> by composing with projection I x V -> V, which is a retract of the= =20 > >> >> generating trivial cofibration and so also a trivial cofibration. I= f=20 > a=20 > >> >> map=20 > >> >> has the rlp against all such maps, then call it a weak fibration.= =20 > Then=20 > >> >> I=20 > >> >> think the resulting awfs of "weak fibrant replacement" should be=20 > stable=20 > >> >> under pullback (although of course, the right maps in the=20 > factorisation=20 > >> >> are=20 > >> >> only weak fibrations, not fibrations in general).=20 > >> >>=20 > >> >> Then eg for propositional truncation, construct the "fibrant=20 > >> >> truncation"=20 > >> >> monad by the coproduct of truncation monad with weak fibrant=20 > >> >> replacement. In=20 > >> >> 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|| ->= =20 > Y=20 > >> >> should=20 > >> >> be also. I think the way to formulate this would be as a=20 > distributive=20 > >> >> law -=20 > >> >> the fibrant replacement monad distributes over the (truncation +=20 > weak=20 > >> >> fibrant replacement) monad. It looks to me like the same thing that= =20 > >> >> works in=20 > >> >> cubical sets should also work here - first define a "box flattening= "=20 > >> >> operation for any fibration (i.e. the operation labelled as=20 > "forward"=20 > >> >> in=20 > >> >> Thierry's note), then show that this operation lifts through the HI= T=20 > >> >> constructors to give a box flattening operation on the HIT, then=20 > show=20 > >> >> that=20 > >> >> in general weak fibration plus box flattening implies fibration,=20 > (Maybe=20 > >> >> one=20 > >> >> way to do this would be to note that the cubical set argument is=20 > mostly=20 > >> >> done=20 > >> >> internally in cubical type theory, and simplicial sets model cubica= l=20 > >> >> type=20 > >> >> theory by Orton & Pitts, Axioms for Modelling Cubical Type Theory i= n=20 > a=20 > >> >> Topos)=20 > >> >>=20 > >> >> Best,=20 > >> >> Andrew=20 > >> >>=20 > >> >>=20 > >> >>=20 > >> >> On Thursday, 1 June 2017 18:08:58 UTC+2, Peter LeFanu Lumsdaine=20 > wrote:=20 > >> >>>=20 > >> >>> On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey =20 > wrote:=20 > >> >>> >=20 > >> >>> > you mean the propositional truncation or suspension operations= =20 > might=20 > >> >>> > lead to cardinals outside of a Grothendieck Universe?=20 > >> >>>=20 > >> >>> Exactly, yes. There=E2=80=99s no reason I know of to think they *= need* to,=20 > >> >>> but=20 > >> >>> with the construction of Mike=E2=80=99s and my paper, they do. An= d adding=20 > >> >>> stronger=20 > >> >>> conditions on the cardinal used won=E2=80=99t help. The problem i= s that=20 > one=20 > >> >>> takes a=20 > >> >>> fibrant replacement to go from the =E2=80=9Cpre-suspension=E2=80= =9D to the=20 > suspension=20 > >> >>> (more=20 > >> >>> precisely: a (TC,F) factorisation, to go from the universal family= =20 > of=20 > >> >>> pre-suspensions to the universal family of suspensions); and=20 > fibrant=20 > >> >>> replacement blows up the fibers to be the size of the *base* of th= e=20 > >> >>> family.=20 > >> >>> So the pre-suspension is small, but the suspension =E2=80=94 altho= ugh=20 > >> >>> essentially=20 > >> >>> small =E2=80=94 ends up as large as the universe one=E2=80=99s usi= ng.=20 > >> >>>=20 > >> >>> So here=E2=80=99s a very precise problem which is as far as I know= open:=20 > >> >>>=20 > >> >>> (*) Construct an operation =CE=A3 : U =E2=80=93> U, where U is Voe= vodsky=E2=80=99s=20 > >> >>> universe,=20 > >> >>> together with appropriate maps N, S : =C3=9B =E2=80=93> =C3=9B ove= r =CE=A3, and a homotopy=20 > m=20 > >> >>> from N=20 > >> >>> to S over =CE=A3, which together exhibit U as =E2=80=9Cclosed unde= r suspension=E2=80=9D.=20 > >> >>>=20 > >> >>> I asked a related question on mathoverflow a couple of years ago:= =20 > >> >>>=20 > >> >>>=20 > https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibrew= ise-suspension-of-fibrations-in-simplicial-sets=20 > >> >>> David White suggested he could see an answer to that question=20 > (which=20 > >> >>> would=20 > >> >>> probably also answer (*) here) based on the comments by Karol=20 > Szumi=C5=82o=20 > >> >>> and=20 > >> >>> Tyler Lawson, using the adjunction with Top, but I wasn=E2=80=99t = quite=20 > able=20 > >> >>> to=20 > >> >>> piece it together.=20 > >> >>>=20 > >> >>> =E2=80=93p.=20 > >> >>>=20 > >> >>> >=20 > >> >>> > > On Jun 1, 2017, at 11:38 AM, Michael Shulman < > shu...@sandiego.edu>=20 > >> >>> > > wrote:=20 > >> >>> > >=20 > >> >>> > > Do we actually know that the Kan simplicial set model has a=20 > >> >>> > > *universe=20 > >> >>> > > closed under* even simple HITs? It's not trivial because this= =20 > >> >>> > > would=20 > >> >>> > > mean we could (say) propositionally truncate or suspend the=20 > >> >>> > > generic=20 > >> >>> > > small Kan fibration and get another *small* Kan fibration,=20 > whereas=20 > >> >>> > > the=20 > >> >>> > > base of these fibrations is not small, and fibrant replacement= =20 > >> >>> > > doesn't=20 > >> >>> > > in general preserve smallness of fibrations with large base=20 > >> >>> > > spaces.=20 > >> >>> > >=20 > >> >>> > > (Also, the current L-S paper doesn't quite give a general=20 > >> >>> > > syntactic=20 > >> >>> > > scheme, only a general semantic framework with suggestive=20 > >> >>> > > implications=20 > >> >>> > > for the corresponding syntax.)=20 > >> >>> > >=20 > >> >>> > >=20 > >> >>> > >=20 > >> >>> > > On Thu, Jun 1, 2017 at 8:30 AM, Steve Awodey = =20 > >> >>> > > wrote:=20 > >> >>> > >>=20 > >> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand=20 > >> >>> > >> =20 > >> >>> > >> wrote:=20 > >> >>> > >>=20 > >> >>> > >> If we are only interested in providing one -particular- mode= l=20 > of=20 > >> >>> > >> HITs,=20 > >> >>> > >> the paper=20 > >> >>> > >> on cubical type theory describes a way to interpret HIT=20 > >> >>> > >> together=20 > >> >>> > >> with a=20 > >> >>> > >> univalent=20 > >> >>> > >> universe which is stable by HIT operations. This gives in=20 > >> >>> > >> particular=20 > >> >>> > >> the=20 > >> >>> > >> consistency=20 > >> >>> > >> and the proof theoretic power of this extension of type=20 > theory.=20 > >> >>> > >>=20 > >> >>> > >>=20 > >> >>> > >> but the Kan simplicial set model already does this =E2=80=94 = right?=20 > >> >>> > >> don=E2=80=99t get me wrong =E2=80=94 I love the cubes, and th= ey have lots of=20 > nice=20 > >> >>> > >> properties=20 > >> >>> > >> for models of HoTT=20 > >> >>> > >> =E2=80=94 but there was never really a question of the consis= tency or=20 > >> >>> > >> coherence of=20 > >> >>> > >> simple HITs like propositional truncation or suspension.=20 > >> >>> > >>=20 > >> >>> > >> the advance in the L-S paper is to give a general scheme for= =20 > >> >>> > >> defining HITs=20 > >> >>> > >> syntactically=20 > >> >>> > >> (a definition, if you like, of what a HIT is, rather than a= =20 > >> >>> > >> family=20 > >> >>> > >> of=20 > >> >>> > >> examples),=20 > >> >>> > >> and then a general description of the semantics of these,=20 > >> >>> > >> in a range of models of the basic theory.=20 > >> >>> > >>=20 > >> >>> > >> Steve=20 > >> >>> > >>=20 > >> >>> > >>=20 > >> >>> > >> The approach uses an operation of =E2=80=9Cflattening an op= en box=E2=80=9D,=20 > >> >>> > >> which=20 > >> >>> > >> solves=20 > >> >>> > >> in=20 > >> >>> > >> this case the issue of interpreting HIT with parameters (such= =20 > as=20 > >> >>> > >> propositional=20 > >> >>> > >> truncation or suspension) without any coherence issue.=20 > >> >>> > >> Since the syntax used in this paper is so close to the=20 > semantics,=20 > >> >>> > >> we=20 > >> >>> > >> limited=20 > >> >>> > >> ourselves to a syntactical presentation of this=20 > interpretation.=20 > >> >>> > >> But=20 > >> >>> > >> it can=20 > >> >>> > >> directly=20 > >> >>> > >> be transformed to a semantical interpretation, as explained i= n=20 > >> >>> > >> the=20 > >> >>> > >> following=20 > >> >>> > >> note=20 > >> >>> > >> (which also incorporates a nice simplification of the=20 > operation=20 > >> >>> > >> of=20 > >> >>> > >> flattering=20 > >> >>> > >> an open box noticed by my coauthors). I also try to make more= =20 > >> >>> > >> explicit in=20 > >> >>> > >> the note=20 > >> >>> > >> what is the problem solved by the =E2=80=9Cflattening boxes= =E2=80=9D method.=20 > >> >>> > >>=20 > >> >>> > >> Only the cases of the spheres and propositional truncation ar= e=20 > >> >>> > >> described,=20 > >> >>> > >> but one=20 > >> >>> > >> would expect the method to generalise to other HITs covered= =20 > e.g.=20 > >> >>> > >> in=20 > >> >>> > >> the HoTT=20 > >> >>> > >> book.=20 > >> >>> > >>=20 > >> >>> > >> On 25 May 2017, at 20:25, Michael Shulman =20 > > >> >>> > >> wrote:=20 > >> >>> > >>=20 > >> >>> > >> The following long-awaited paper is now available:=20 > >> >>> > >>=20 > >> >>> > >> Semantics of higher inductive types=20 > >> >>> > >> Peter LeFanu Lumsdaine, Mike Shulman=20 > >> >>> > >> https://arxiv.org/abs/1705.07088=20 > >> >>> > >>=20 > >> >>> > >> From the abstract:=20 > >> >>> > >>=20 > >> >>> > >> We introduce the notion of *cell monad with parameters*: a=20 > >> >>> > >> semantically-defined scheme for specifying homotopically=20 > >> >>> > >> well-behaved=20 > >> >>> > >> notions of structure. We then show that any suitable model=20 > >> >>> > >> category=20 > >> >>> > >> has *weakly stable typal initial algebras* for any cell monad= =20 > >> >>> > >> with=20 > >> >>> > >> parameters. When combined with the local universes=20 > construction=20 > >> >>> > >> to=20 > >> >>> > >> obtain strict stability, this specializes to give models of= =20 > >> >>> > >> specific=20 > >> >>> > >> higher inductive types, including spheres, the torus, pushout= =20 > >> >>> > >> types,=20 > >> >>> > >> truncations, the James construction, and general=20 > localisations.=20 > >> >>> > >>=20 > >> >>> > >> Our results apply in any sufficiently nice Quillen model=20 > >> >>> > >> category,=20 > >> >>> > >> including any right proper simplicial Cisinski model category= =20 > >> >>> > >> (such=20 > >> >>> > >> as=20 > >> >>> > >> simplicial sets) and any locally presentable locally cartesia= n=20 > >> >>> > >> closed=20 > >> >>> > >> category (such as sets) with its trivial model structure. In= =20 > >> >>> > >> particular, any locally presentable locally cartesian closed= =20 > >> >>> > >> (=E2=88=9E,1)-category is presented by some model category to= which=20 > our=20 > >> >>> > >> results apply.=20 > >> >>> > >>=20 > >> >>> > >> --=20 > >> >>> > >> You received this message because you are subscribed to the= =20 > >> >>> > >> Google=20 > >> >>> > >> Groups=20 > >> >>> > >> "Homotopy Type Theory" group.=20 > >> >>> > >> To unsubscribe from this group and stop receiving emails from= =20 > it,=20 > >> >>> > >> send an=20 > >> >>> > >> email to HomotopyTypeThe...@googlegroups.com=20 > .=20 > >> >>> > >> For more options, visit https://groups.google.com/d/optout.= =20 > >> >>> > >>=20 > >> >>> > >>=20 > >> >>> > >>=20 > >> >>> > >> --=20 > >> >>> > >> You received this message because you are subscribed to the= =20 > >> >>> > >> Google=20 > >> >>> > >> Groups=20 > >> >>> > >> "Homotopy Type Theory" group.=20 > >> >>> > >> To unsubscribe from this group and stop receiving emails from= =20 > it,=20 > >> >>> > >> send an=20 > >> >>> > >> email to HomotopyTypeThe...@googlegroups.com=20 > .=20 > >> >>> > >> For more options, visit https://groups.google.com/d/optout.= =20 > >> >>> > >>=20 > >> >>> > >>=20 > >> >>> > >> --=20 > >> >>> > >> You received this message because you are subscribed to the= =20 > >> >>> > >> Google=20 > >> >>> > >> Groups=20 > >> >>> > >> "Homotopy Type Theory" group.=20 > >> >>> > >> To unsubscribe from this group and stop receiving emails from= =20 > it,=20 > >> >>> > >> send an=20 > >> >>> > >> email to HomotopyTypeThe...@googlegroups.com=20 > .=20 > >> >>> > >> For more options, visit https://groups.google.com/d/optout.= =20 > >> >>> > >=20 > >> >>> > > --=20 > >> >>> > > You received this message because you are subscribed to the=20 > Google=20 > >> >>> > > Groups "Homotopy Type Theory" group.=20 > >> >>> > > To unsubscribe from this group and stop receiving emails from= =20 > it,=20 > >> >>> > > send an email to=20 > HomotopyTypeThe...@googlegroups.com .=20 > >> >>> > > For more options, visit https://groups.google.com/d/optout.=20 > >> >>> >=20 > >> >>> > --=20 > >> >>> > You received this message because you are subscribed to the=20 > Google=20 > >> >>> > Groups "Homotopy Type Theory" group.=20 > >> >>> > To unsubscribe from this group and stop receiving emails from it= ,=20 > >> >>> > send=20 > >> >>> > an email to HomotopyTypeThe...@googlegroups.com=20 > .=20 > >> >>> > For more options, visit https://groups.google.com/d/optout.=20 > >> >=20 > >> > --=20 > >> > You received this message because you are subscribed to the Google= =20 > >> > Groups=20 > >> > "Homotopy Type Theory" group.=20 > >> > To unsubscribe from this group and stop receiving emails from it,=20 > send=20 > >> > an=20 > >> > email to HomotopyTypeThe...@googlegroups.com=20 > .=20 > >> > For more options, visit https://groups.google.com/d/optout.=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups=20 > > "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > > email to HomotopyTypeThe...@googlegroups.com .=20 > > For more options, visit https://groups.google.com/d/optout.=20 > ------=_Part_1920_891118772.1496782751459 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
I don't have a clear idea - the only examples I know o= f are simplicial sets, variants of cubical sets and the effective topos. Al= so I don't know which HITs can be done with this kind of approach.
=

On Tuesday, 6 June 2017 21:36:56 UTC+2, Michael Shulman wrote= :
What class of homotopy theori= es can be presented by such models?

On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan <wake...@gmail.com> w= rote:
> I don't know how general this is exactly in practice, but I th= ink it should
> work in the setting that appears in van de Berg, Frumin A homotopy= -theoretic
> model of function extensionality in the effective topos, which reg= ardless of
> the title is not just the effective topos, but any topos together = with a
> interval object with connections, a dominance satisfying certain c= onditions,
> with fibrations defined as maps with the rlp against pushout produ= ct of
> endpoint inclusions and elements of the dominance (& in additi= on there
> should be some more conditions to ensure that free monads on point= ed
> endofunctors exist).
>
>
> I'm a bit more confident that it works now. The class of weak = fibrations is
> not cofibrantly generated in the usual sense (as I claimed in the = first
> post), but they are in the more general sense by Christian Sattler= in
> section 6 of The Equivalence Extension Property and Model Structur= es. Then a
> version of step 1 of the small object argument applies to Christia= n's
> definition, which gives a pointed endofunctor whose algebras are t= he weak
> fibrations. The same technique can also be used to describe "= box flattening"
> (which should probably be called something else, like "cylind= er flattening"
> in the general setting).
>
>
> Andrew
>
> On Tuesday, 6 June 2017 15:35:36 UTC+2, Michael Shulman wrote:
>>
>> I'll be interested to see if you can make it work!
>>
>> But I'd be much more interested if there is something that= can be done
>> in a general class of models, rather than a particular one lik= e
>> cubical or simplicial sets.
>>
>> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan <wake...@gma= il.com> wrote:
>> > Actually, I've just noticed that doesn't quite wo= rk - I want to say that
>> > a
>> > map is a weak fibration if it has a (uniform choice of) d= iagonal fillers
>> > for
>> > lifting problems against generating cofibrations where th= e bottom map
>> > factors through the projection I x V -> V, but that do= esn't seem to be
>> > cofibrantly generated. Maybe it's still possible to d= o something like
>> > 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 l= ooking at the HITs in
>> >> cubical type theory, and I don't have a complete = proof, but I think
>> >> actually
>> >> the same sort of thing should work for simplicial set= s.
>> >>
>> >> We already know that the fibrations in the usual mode= l structure on
>> >> simplicial sets can be defined as maps with the rlp a= gainst the pushout
>> >> product of generating cofibrations with interval endp= oint inclusions
>> >> (in
>> >> Christian's new paper on model structures he cite= s for this result
>> >> Chapter
>> >> IV, section 2 of P. Gabriel and M. Zisman. Calculus o= f fractions and
>> >> homotopy theory, but I'm not familiar with the pr= oof myself).
>> >>
>> >> Now a generating trivial cofibration is the pushout p= roduct of a
>> >> generating cofibration with endpoint inclusion, so it= s codomain is of
>> >> the
>> >> form I x V, where V is the codomain of the generating= cofibration
>> >> (which for
>> >> cubical sets and simplicial sets is representable). T= hen we get another
>> >> map
>> >> by composing with projection I x V -> V, which is = a retract of the
>> >> generating trivial cofibration and so also a trivial = cofibration. If a
>> >> map
>> >> has the rlp against all such maps, then call it a wea= k fibration. Then
>> >> I
>> >> think the resulting awfs of "weak fibrant replac= ement" should be stable
>> >> under pullback (although of course, the right maps in= the factorisation
>> >> are
>> >> only weak fibrations, not fibrations in general).
>> >>
>> >> Then eg for propositional truncation, construct the &= quot;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 this would be a= s a distributive
>> >> law -
>> >> the fibrant replacement monad distributes over the (t= runcation + weak
>> >> fibrant replacement) monad. It looks to me like the s= ame thing that
>> >> works in
>> >> cubical sets should also work here - first define a &= quot;box flattening"
>> >> operation for any fibration (i.e. the operation label= led as "forward"
>> >> in
>> >> Thierry's note), then show that this operation li= fts through the HIT
>> >> constructors to give a box flattening operation on th= e HIT, then show
>> >> that
>> >> in general weak fibration plus box flattening implies= fibration, (Maybe
>> >> one
>> >> way to do this would be to note that the cubical set = argument is mostly
>> >> done
>> >> internally in cubical type theory, and simplicial set= s model cubical
>> >> type
>> >> theory by Orton & Pitts, Axioms for Modelling Cub= ical 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 propositional truncation or sus= pension operations might
>> >>> > lead to cardinals outside of a Grothendieck = Universe?
>> >>>
>> >>> Exactly, yes. =C2=A0There=E2=80=99s no reason I k= now of to think they *need* to,
>> >>> but
>> >>> with the construction of Mike=E2=80=99s and my pa= per, they do. =C2=A0And adding
>> >>> stronger
>> >>> conditions on the cardinal used won=E2=80=99t hel= p. =C2=A0The problem is that one
>> >>> takes a
>> >>> fibrant replacement to go from the =E2=80=9Cpre-s= uspension=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 suspen= sions); 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 suspensio= n =E2=80=94 although
>> >>> 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&g= t; 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 suspension=E2=80=9D.
>> >>>
>> >>> I asked a related question on mathoverflow a coup= le of years ago:
>> >>>
>> >>> https://mathoverflow.net/questions/219588/pullback-stab= le-model-of-fibrewise-suspension-of-fibrations-in-simplicial-sets=
>> >>> David White suggested he could see an answer to t= hat question (which
>> >>> would
>> >>> probably also answer (*) here) based on the comme= nts 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.
>> >>>
>> >>> >
>> >>> > > On Jun 1, 2017, at 11:38 AM, Michael Sh= ulman <shu...@sandiego.edu>
>> >>> > > wrote:
>> >>> > >
>> >>> > > Do we actually know that the Kan simpli= cial set model has a
>> >>> > > *universe
>> >>> > > closed under* even simple HITs? =C2=A0I= t's not trivial because this
>> >>> > > would
>> >>> > > mean we could (say) propositionally tru= ncate or suspend the
>> >>> > > generic
>> >>> > > small Kan fibration and get another *sm= all* Kan fibration, whereas
>> >>> > > the
>> >>> > > base of these fibrations is not small, = and fibrant replacement
>> >>> > > doesn't
>> >>> > > in general preserve smallness of fibrat= ions with large base
>> >>> > > spaces.
>> >>> > >
>> >>> > > (Also, the current L-S paper doesn'= t quite give a general
>> >>> > > syntactic
>> >>> > > scheme, only a general semantic framewo= rk with suggestive
>> >>> > > implications
>> >>> > > for the corresponding syntax.)
>> >>> > >
>> >>> > >
>> >>> > >
>> >>> > > On Thu, Jun 1, 2017 at 8:30 AM, Steve A= wodey <awo...@cmu.edu>
>> >>> > > wrote:
>> >>> > >>
>> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierr= y Coquand
>> >>> > >> <Thier...@cse.gu.se>
>> >>> > >> wrote:
>> >>> > >>
>> >>> > >> =C2=A0If we are only interested 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 ope= rations. This gives in
>> >>> > >> particular
>> >>> > >> the
>> >>> > >> consistency
>> >>> > >> and the proof theoretic power of th= is extension of type theory.
>> >>> > >>
>> >>> > >>
>> >>> > >> but the Kan simplicial set model al= ready does this =E2=80=94 right?
>> >>> > >> 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
>> >>> > >> =E2=80=94 but there was never reall= y a question of the consistency or
>> >>> > >> coherence of
>> >>> > >> simple HITs like propositional trun= cation 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 t= he semantics of these,
>> >>> > >> in a range of models of the basic t= heory.
>> >>> > >>
>> >>> > >> Steve
>> >>> > >>
>> >>> > >>
>> >>> > >> =C2=A0The approach uses an operatio= n of =C2=A0=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 a= ny coherence issue.
>> >>> > >> Since the syntax used in this paper= is so close to the semantics,
>> >>> > >> we
>> >>> > >> limited
>> >>> > >> ourselves =C2=A0to a syntactical pr= esentation of this interpretation.
>> >>> > >> But
>> >>> > >> it can
>> >>> > >> directly
>> >>> > >> be transformed to a semantical inte= rpretation, as explained in
>> >>> > >> the
>> >>> > >> following
>> >>> > >> note
>> >>> > >> (which also incorporates a nice sim= plification 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 method.
>> >>> > >>
>> >>> > >> Only the cases of the spheres and p= ropositional truncation are
>> >>> > >> described,
>> >>> > >> but one
>> >>> > >> would expect the method to generali= se to other HITs covered e.g.
>> >>> > >> in
>> >>> > >> the HoTT
>> >>> > >> book.
>> >>> > >>
>> >>> > >> On 25 May 2017, at 20:25, Michael S= hulman <shu...@sandiego.edu>
>> >>> > >> wrote:
>> >>> > >>
>> >>> > >> The following long-awaited paper is= now available:
>> >>> > >>
>> >>> > >> Semantics of higher inductive types
>> >>> > >> Peter LeFanu Lumsdaine, Mike Shulma= n
>> >>> > >> https://arxiv.org/a= bs/1705.07088
>> >>> > >>
>> >>> > >> From the abstract:
>> >>> > >>
>> >>> > >> We introduce the notion of *cell mo= nad with parameters*: a
>> >>> > >> semantically-defined scheme for spe= cifying homotopically
>> >>> > >> well-behaved
>> >>> > >> notions of structure. We then show = that any suitable model
>> >>> > >> category
>> >>> > >> has *weakly stable typal initial al= gebras* for any cell monad
>> >>> > >> with
>> >>> > >> parameters. When combined with the = local universes construction
>> >>> > >> to
>> >>> > >> obtain strict stability, this speci= alizes to give models of
>> >>> > >> specific
>> >>> > >> higher inductive types, including s= pheres, the torus, pushout
>> >>> > >> types,
>> >>> > >> truncations, the James construction= , and general localisations.
>> >>> > >>
>> >>> > >> Our results apply in any sufficient= ly nice Quillen model
>> >>> > >> category,
>> >>> > >> including any right proper simplici= al Cisinski model category
>> >>> > >> (such
>> >>> > >> as
>> >>> > >> simplicial sets) and any locally pr= esentable locally cartesian
>> >>> > >> closed
>> >>> > >> category (such as sets) with its tr= ivial 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 y= ou are subscribed to the
>> >>> > >> Google
>> >>> > >> Groups
>> >>> > >> "Homotopy Type Theory" gr= oup.
>> >>> > >> To unsubscribe from this group and = stop receiving emails from it,
>> >>> > >> send an
>> >>> > >> email to HomotopyTypeTheory+unsub..= .@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >>
>> >>> > >>
>> >>> > >>
>> >>> > >> --
>> >>> > >> You received this message because y= ou are subscribed to the
>> >>> > >> Google
>> >>> > >> Groups
>> >>> > >> "Homotopy Type Theory" gr= oup.
>> >>> > >> To unsubscribe from this group and = stop receiving emails from it,
>> >>> > >> send an
>> >>> > >> email to HomotopyTypeTheory+unsub..= .@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >>
>> >>> > >>
>> >>> > >> --
>> >>> > >> You received this message because y= ou are subscribed to the
>> >>> > >> Google
>> >>> > >> Groups
>> >>> > >> "Homotopy Type Theory" gr= oup.
>> >>> > >> To unsubscribe from this group and = stop receiving emails from it,
>> >>> > >> send an
>> >>> > >> email to HomotopyTypeTheory+unsub..= .@googlegroups.com.
>> >>> > >> For more options, visit https://groups.google.com/d/optout.
>> >>> > >
>> >>> > > --
>> >>> > > You received this message because you a= re subscribed to the Google
>> >>> > > Groups "Homotopy Type Theory"= group.
>> >>> > > To unsubscribe from this group and stop= receiving emails from it,
>> >>> > > send an email to HomotopyTypeTheory+uns= ub...@googlegroups.com.
>> >>> > > For more options, visit https://groups.google.com/d/optout.
>> >>> >
>> >>> > --
>> >>> > You received this message because you are su= bscribed to the Google
>> >>> > Groups "Homotopy Type Theory" grou= p.
>> >>> > To unsubscribe from this group and stop rece= iving emails from it,
>> >>> > send
>> >>> > an email to HomotopyTypeTheory+unsub...@go= oglegroups.com.
>> >>> > For more options, visit https://groups.google.com/d/optout.
>> >
>> > --
>> > You received this message because you are subscribed to t= he Google
>> > Groups
>> > "Homotopy Type Theory" group.
>> > To unsubscribe from this group and stop receiving emails = from it, send
>> > an
>> > email to HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.
------=_Part_1920_891118772.1496782751459-- ------=_Part_1919_1893536486.1496782751457--