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