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.

------=_Part_1920_891118772.1496782751459--
------=_Part_1919_1893536486.1496782751457--
=

On Tuesday, 6 June 2017 21:36:56 UTC+2, Michael Shulman wrote= :

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

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

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

>> >>> > >> 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. https:= //groups.google.com/d/

>> > For more options, visitoptout .

>

> --

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