I don't have a clear idea - the only examples I know of are simplicial sets, variants of cubical sets and the effective topos. Also 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 theories can be presented by such models? > > On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan > wrote: > > I don't know how general this is exactly in practice, but I think 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 > regardless of > > the title is not just the effective topos, but any topos together with a > > interval object with connections, a dominance satisfying certain > conditions, > > with fibrations defined as maps with the rlp against pushout product of > > endpoint inclusions and elements of the dominance (& in addition there > > should be some more conditions to ensure that free monads on pointed > > 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 Structures. > Then a > > version of step 1 of the small object argument applies to Christian's > > definition, which gives a pointed endofunctor whose algebras are the > weak > > fibrations. The same technique can also be used to describe "box > flattening" > > (which should probably be called something else, like "cylinder > 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 like > >> cubical or simplicial sets. > >> > >> On Tue, Jun 6, 2017 at 4:03 AM, Andrew Swan > wrote: > >> > Actually, I've just noticed that doesn't quite work - I want to say > that > >> > a > >> > map is a weak fibration if it has a (uniform choice of) diagonal > fillers > >> > for > >> > lifting problems against generating cofibrations where the bottom map > >> > factors through the projection I x V -> V, but that doesn't seem to > be > >> > cofibrantly generated. Maybe it's still possible to do 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 looking 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 sets. > >> >> > >> >> We already 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 generating 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 fractions and > >> >> homotopy theory, but I'm not familiar with the proof myself). > >> >> > >> >> Now a generating trivial cofibration is the pushout product of a > >> >> generating cofibration with endpoint inclusion, so its 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). Then 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 weak fibration. > 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). > >> >> > >> >> Then eg for propositional truncation, construct the "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 as a > distributive > >> >> law - > >> >> the fibrant replacement monad distributes over the (truncation + > weak > >> >> fibrant replacement) monad. It looks to me like the same thing that > >> >> works in > >> >> cubical sets should also work here - first define a "box flattening" > >> >> operation for any fibration (i.e. the operation labelled as > "forward" > >> >> in > >> >> Thierry's note), then show that this operation lifts through the HIT > >> >> constructors to give a box flattening 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 note that the cubical set argument is > mostly > >> >> done > >> >> internally in cubical type theory, and simplicial sets model cubical > >> >> type > >> >> theory by Orton & Pitts, Axioms 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 > wrote: > >> >>> > > >> >>> > you mean the propositional truncation or suspension operations > might > >> >>> > lead to cardinals outside of a Grothendieck Universe? > >> >>> > >> >>> Exactly, yes. There’s no reason I know of to think they *need* to, > >> >>> but > >> >>> with the construction of Mike’s and my paper, they do. And adding > >> >>> stronger > >> >>> conditions on the cardinal used won’t help. The problem is that > one > >> >>> takes a > >> >>> fibrant replacement to go from the “pre-suspension” to the > suspension > >> >>> (more > >> >>> precisely: a (TC,F) factorisation, to go from the universal family > of > >> >>> pre-suspensions to the universal family of suspensions); 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 suspension — although > >> >>> essentially > >> >>> small — ends up as large as the universe one’s using. > >> >>> > >> >>> So here’s a very precise problem which is as far as I know open: > >> >>> > >> >>> (*) Construct an operation Σ : U –> U, where U is Voevodsky’s > >> >>> universe, > >> >>> together with appropriate maps N, S : Û –> Û over Σ, and a homotopy > m > >> >>> from N > >> >>> to S over Σ, which together exhibit U as “closed under suspension”. > >> >>> > >> >>> I asked a related question on mathoverflow a couple of years ago: > >> >>> > >> >>> > https://mathoverflow.net/questions/219588/pullback-stable-model-of-fibrewise-suspension-of-fibrations-in-simplicial-sets > >> >>> David White suggested he could see an answer to that question > (which > >> >>> would > >> >>> probably also answer (*) here) based on the comments by Karol > Szumiło > >> >>> and > >> >>> Tyler Lawson, using the adjunction with Top, but I wasn’t quite > able > >> >>> to > >> >>> piece it together. > >> >>> > >> >>> –p. > >> >>> > >> >>> > > >> >>> > > 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? 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 > >> >>> > > 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 > >> >>> > > scheme, only a general semantic framework with suggestive > >> >>> > > implications > >> >>> > > 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 > >> >>> > >> HITs, > >> >>> > >> the paper > >> >>> > >> on cubical type theory describes a way to interpret HIT > >> >>> > >> together > >> >>> > >> with a > >> >>> > >> univalent > >> >>> > >> universe which is stable by HIT operations. This gives in > >> >>> > >> particular > >> >>> > >> the > >> >>> > >> consistency > >> >>> > >> and the proof theoretic power of this extension of type > theory. > >> >>> > >> > >> >>> > >> > >> >>> > >> but the Kan simplicial set model already does this — right? > >> >>> > >> don’t get me wrong — I love the cubes, and they have lots of > nice > >> >>> > >> properties > >> >>> > >> for models of HoTT > >> >>> > >> — but there was never really a question of the consistency or > >> >>> > >> coherence of > >> >>> > >> simple HITs like propositional truncation 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 the semantics of these, > >> >>> > >> in a range of models of the basic theory. > >> >>> > >> > >> >>> > >> Steve > >> >>> > >> > >> >>> > >> > >> >>> > >> The approach uses an operation of “flattening an open box”, > >> >>> > >> which > >> >>> > >> 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. > >> >>> > >> But > >> >>> > >> it can > >> >>> > >> directly > >> >>> > >> be transformed to a semantical interpretation, as explained in > >> >>> > >> the > >> >>> > >> 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 > >> >>> > >> explicit in > >> >>> > >> the note > >> >>> > >> what is the problem solved by the “flattening boxes” method. > >> >>> > >> > >> >>> > >> Only the cases of the spheres and propositional truncation are > >> >>> > >> described, > >> >>> > >> but one > >> >>> > >> would expect the method to generalise to other HITs covered > e.g. > >> >>> > >> in > >> >>> > >> the HoTT > >> >>> > >> book. > >> >>> > >> > >> >>> > >> On 25 May 2017, at 20:25, Michael Shulman > > >> >>> > >> 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-behaved > >> >>> > >> 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 > >> >>> > >> specific > >> >>> > >> 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 > >> >>> > >> as > >> >>> > >> simplicial sets) and any locally presentable locally cartesian > >> >>> > >> closed > >> >>> > >> category (such as sets) with its trivial model structure. In > >> >>> > >> particular, any locally presentable locally cartesian closed > >> >>> > >> (∞,1)-category is presented by some model category to which > our > >> >>> > >> results apply. > >> >>> > >> > >> >>> > >> -- > >> >>> > >> 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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 > HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com . > > For more options, visit https://groups.google.com/d/optout. >