Re: [HoTT] Semantics of higher inductive types

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

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

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 <wake...@gmail.com 
> <javascript:>> 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 <wake...@gmail.com> 
> 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. 
> > 
> > -- 
> > 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: 28432 bytes --]