Re: [HoTT] Semantics of higher inductive types

[Andrew Swan <wakeli...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 14841 bytes --]

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 
<https://arxiv.org/pdf/1701.08369.pdf>, 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 
<https://arxiv.org/pdf/1704.06911>. 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 <wake...@gmail.com 
> <javascript:>> 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 <awo...@cmu.edu> 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 <awo...@cmu.edu> 
> wrote: 
> >>> > >> 
> >>> > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <
> Thier...@cse.gu.se> 
> >>> > >> 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 <shu...@sandiego.edu> 
> >>> > >> 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 
> <javascript:>. 
> >>> > >> 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 
> <javascript:>. 
> >>> > >> 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 
> <javascript:>. 
> >>> > >> 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 
> <javascript:>. 
> >>> > > 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 
> <javascript:>. 
> >>> > 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 <javascript:>. 
> > For more options, visit https://groups.google.com/d/optout. 
>

[-- Attachment #1.2: Type: text/html, Size: 22833 bytes --]