* Semantics of higher inductive types @ 2017-05-25 18:25 Michael Shulman 2017-05-26 0:17 ` [HoTT] " Emily Riehl 2017-06-01 14:23 ` Thierry Coquand 0 siblings, 2 replies; 25+ messages in thread From: Michael Shulman @ 2017-05-25 18:25 UTC (permalink / raw) To: HomotopyT...@googlegroups.com 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-05-25 18:25 Semantics of higher inductive types Michael Shulman @ 2017-05-26 0:17 ` Emily Riehl 2017-06-01 14:23 ` Thierry Coquand 1 sibling, 0 replies; 25+ messages in thread From: Emily Riehl @ 2017-05-26 0:17 UTC (permalink / raw) To: HomotopyT...@googlegroups.com [-- Attachment #1: Type: text/plain, Size: 1980 bytes --] Mike gave a fantastic introduction to this work geared to a more homotopically-oriented audience a year ago at Johns Hopkins. Slides are available here: http://home.sandiego.edu/~shulman/papers/cellcxs.pdf <http://home.sandiego.edu/~shulman/papers/cellcxs.pdf> It’s beautiful mathematics. I’m really excited that this paper has now appeared. Congratulations Mike and Peter! Emily > On May 26, 2017, at 4:25 AM, 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. > For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 2983 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-05-25 18:25 Semantics of higher inductive types Michael Shulman 2017-05-26 0:17 ` [HoTT] " Emily Riehl @ 2017-06-01 14:23 ` Thierry Coquand 2017-06-01 14:43 ` Michael Shulman 2017-06-01 15:30 ` Steve Awodey 1 sibling, 2 replies; 25+ messages in thread From: Thierry Coquand @ 2017-06-01 14:23 UTC (permalink / raw) To: homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 2824 bytes --] If we are only interested in providing one -particular- model of HITs, the paper<https://arxiv.org/abs/1611.02108> 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. 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<http://www.cse.chalmers.se/~coquand/hit3.pdf> (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<mailto: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. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4290 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 14:23 ` Thierry Coquand @ 2017-06-01 14:43 ` Michael Shulman 2017-06-01 15:30 ` Steve Awodey 1 sibling, 0 replies; 25+ messages in thread From: Michael Shulman @ 2017-06-01 14:43 UTC (permalink / raw) To: Thierry Coquand; +Cc: homotopy Type Theory Yes, this is something rather mysterious to me. There may be something special about the cubical model that enables a sort of "horizontal/vertical" decomposition of fibrations. Peter and I thought for a little while about whether there is some similar sort of "fiberwise fibrant replacement" that would work in a general model, but weren't able to come up with anything; however, perhaps we just weren't clever enough. I do think it is very important not to be limited to one particular model. On Thu, Jun 1, 2017 at 7:23 AM, Thierry Coquand <Thierry...@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. > > 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. > 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 14:23 ` Thierry Coquand 2017-06-01 14:43 ` Michael Shulman @ 2017-06-01 15:30 ` Steve Awodey 2017-06-01 15:38 ` Michael Shulman 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA 1 sibling, 2 replies; 25+ messages in thread From: Steve Awodey @ 2017-06-01 15:30 UTC (permalink / raw) To: Thierry Coquand; +Cc: homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 4069 bytes --] > On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote: > > If we are only interested in providing one -particular- model of HITs, the paper <https://arxiv.org/abs/1611.02108> > 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 <http://www.cse.chalmers.se/~coquand/hit3.pdf> > (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 <mailto: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 <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 <mailto:HomotopyTypeThe...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>. [-- Attachment #2: Type: text/html, Size: 6416 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 15:30 ` Steve Awodey @ 2017-06-01 15:38 ` Michael Shulman 2017-06-01 15:56 ` Steve Awodey 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA 1 sibling, 1 reply; 25+ messages in thread From: Michael Shulman @ 2017-06-01 15:38 UTC (permalink / raw) To: Steve Awodey; +Cc: Thierry Coquand, homotopy Type Theory 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 <Thierry...@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. > 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 15:38 ` Michael Shulman @ 2017-06-01 15:56 ` Steve Awodey 2017-06-01 16:08 ` Peter LeFanu Lumsdaine 0 siblings, 1 reply; 25+ messages in thread From: Steve Awodey @ 2017-06-01 15:56 UTC (permalink / raw) To: Michael Shulman; +Cc: Thierry Coquand, homotopy Type Theory you mean the propositional truncation or suspension operations might lead to cardinals outside of a Grothendieck Universe? > 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 <Thierry...@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. >> 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 15:56 ` Steve Awodey @ 2017-06-01 16:08 ` Peter LeFanu Lumsdaine 2017-06-06 9:19 ` Andrew Swan 2017-06-07 9:40 ` Peter LeFanu Lumsdaine 0 siblings, 2 replies; 25+ messages in thread From: Peter LeFanu Lumsdaine @ 2017-06-01 16:08 UTC (permalink / raw) To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 7553 bytes --] 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 <Thierry...@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. > >> 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. [-- Attachment #2: Type: text/html, Size: 9902 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 16:08 ` Peter LeFanu Lumsdaine @ 2017-06-06 9:19 ` Andrew Swan 2017-06-06 10:03 ` Andrew Swan 2017-06-07 9:40 ` Peter LeFanu Lumsdaine 1 sibling, 1 reply; 25+ messages in thread From: Andrew Swan @ 2017-06-06 9:19 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: awo..., shu..., Thierry..., homotopyt... [-- Attachment #1.1: Type: text/plain, Size: 10849 bytes --] 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 <https://arxiv.org/pdf/1704.06911.pdf> 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 <http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf> ) 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 <javascript:>> > 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 > <javascript:>> 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 > <javascript:>> wrote: > > >> > > >> On Jun 1, 2017, at 10:23 AM, Thierry Coquand <Thier...@cse.gu.se > <javascript:>> > > >> 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 > <javascript:>> 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. > [-- Attachment #1.2: Type: text/html, Size: 16728 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-06 9:19 ` Andrew Swan @ 2017-06-06 10:03 ` Andrew Swan 2017-06-06 13:35 ` Michael Shulman 0 siblings, 1 reply; 25+ messages in thread From: Andrew Swan @ 2017-06-06 10:03 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: awo..., shu..., Thierry..., homotopyt... [-- Attachment #1.1: Type: text/plain, Size: 11441 bytes --] 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 <https://arxiv.org/pdf/1704.06911.pdf> 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 > <http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf> > ) > > 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. >> > >> 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. >> > [-- Attachment #1.2: Type: text/html, Size: 16438 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-06 10:03 ` Andrew Swan @ 2017-06-06 13:35 ` Michael Shulman 2017-06-06 16:22 ` Andrew Swan 0 siblings, 1 reply; 25+ messages in thread From: Michael Shulman @ 2017-06-06 13:35 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory, Steve Awodey, Thierry Coquand 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 <wakeli...@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. >>> > >> 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-06 13:35 ` Michael Shulman @ 2017-06-06 16:22 ` Andrew Swan 2017-06-06 19:36 ` Michael Shulman 0 siblings, 1 reply; 25+ messages in thread From: Andrew Swan @ 2017-06-06 16:22 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry... [-- 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 --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-06 16:22 ` Andrew Swan @ 2017-06-06 19:36 ` Michael Shulman 2017-06-06 20:59 ` Andrew Swan 0 siblings, 1 reply; 25+ messages in thread From: Michael Shulman @ 2017-06-06 19:36 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory, Steve Awodey, Thierry Coquand What class of homotopy theories can be presented by such models? On Tue, Jun 6, 2017 at 10:22 AM, Andrew Swan <wakeli...@gmail.com> 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. >> >>> > >> 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-06 19:36 ` Michael Shulman @ 2017-06-06 20:59 ` Andrew Swan 0 siblings, 0 replies; 25+ messages in thread From: Andrew Swan @ 2017-06-06 20:59 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry... [-- 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 --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 16:08 ` Peter LeFanu Lumsdaine 2017-06-06 9:19 ` Andrew Swan @ 2017-06-07 9:40 ` Peter LeFanu Lumsdaine 2017-06-07 9:57 ` Thierry Coquand [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> 1 sibling, 2 replies; 25+ messages in thread From: Peter LeFanu Lumsdaine @ 2017-06-07 9:40 UTC (permalink / raw) To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 4309 bytes --] On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine < p.l.lu...@gmail.com> 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. > I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.) So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) Construction of propositional truncation without size blowup in simplicial sets: (1) Given a fibration Y —> X, define |Y| —> X as follows: an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with a “partial lift of x into Y, defined at least on all vertices”, i.e. a subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that the evident square commutes; reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map). (2) There’s an evident map Y —> |Y| over X; and the operation sending Y to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X. (Straightforward.) (3) In general, a fibration is a proposition in the type-theoretic sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. (Non-trivial but not too hard to check.) (4) The map |Y| —> X is a fibration, and a proposition. (Straightforward, given (3), by concretely constructing the required liftings.) (5) The evident map Y —> |Y| over X is a cell complex constructed from boundary inclusions δ[n] —> Δ[n] with n > 0. To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose “missing” simplices are all of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> Δ[n+1]. (6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably in X. (Orthogonality is immediate from (3) and (5); stability is then by (2).) (7) Let V be either the universe of “well-ordered α-small fibrations”, or the universe of “displayed α-small fibrations”, for α any infinite regular cardinal. Then V carries an operation representing the construction of (1), and modelling propositional truncation. (Lengthy to spell out in full, but straightforward given (2), (6).) –p. [-- Attachment #2: Type: text/html, Size: 5150 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-07 9:40 ` Peter LeFanu Lumsdaine @ 2017-06-07 9:57 ` Thierry Coquand [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> 1 sibling, 0 replies; 25+ messages in thread From: Thierry Coquand @ 2017-06-07 9:57 UTC (permalink / raw) To: Peter LeFanu Lumsdaine; +Cc: homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 2585 bytes --] On 7 Jun 2017, at 11:40, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com<mailto:p.l.lu...@gmail.com>> wrote: On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com<mailto:p.l.lu...@gmail.com>> wrote: On Thu, Jun 1, 2017 at 6:56 PM, Steve Awodey <awo...@cmu.edu<mailto: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. I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.) So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) Yes, suspension can be treated using the method of “flattening open boxes” similarly to propositional truncation (it is actually simpler since it is not recursive). For completeness, I added the description of suspension at the end of this note<http://www.cse.chalmers.se/~coquand/hit3.pdf> of HIT. Thierry [-- Attachment #2: Type: text/html, Size: 3798 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
[parent not found: <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com>]
* Re: [HoTT] Semantics of higher inductive types [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> @ 2017-06-07 23:06 ` Michael Shulman 2017-06-08 6:35 ` Andrew Swan 2018-09-14 11:15 ` Thierry Coquand 1 sibling, 1 reply; 25+ messages in thread From: Michael Shulman @ 2017-06-07 23:06 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory, Steve Awodey, Thierry Coquand On Wed, Jun 7, 2017 at 12:34 PM, Andrew Swan <wakeli...@gmail.com> wrote: > The technique used in cubical type theory seems fairly flexible. I'm not > sure exactly how flexible, but I think I can get suspension to work in > simplicial sets. In the below, throughout I use the characterisation of > fibrations as maps with the rlp against the pushout product of each > monomorphism with endpoint inclusion into the interval. WLOG there is also a > uniformity condition - we have a choice of lift and "pulling back the > monomorphism preserves the lift." Why is there no LOG in this? > Given a fibration X -> Y, you first freely add elements N and S together > with a path from N to S for each element of X (I think this is the same as > what you called pre suspension). Although the pre suspension is not a > fibration in general, it does have some of the properties you might expect > from a fibration. Given a path in Y, and an element in the fibre of an > endpoint, one can transport along the path to get something in the fibre of > the other endpoint. There should also be a "flattening" operation that takes > a path q in presuspension(X) over p in Y, and returns a path from q(1) to > the transport along p of q(0) that lies entirely in the fibre of p(1). > > You then take the "weak fibrant replacement" of the pre suspension. A map > in simplicial sets is a fibration if and only if it has the rlp against each > pushout product of a monomorphism with an endpoint inclusion into the > interval. In fibrant replacement you freely add a diagonal lift for each > such lifting problems. In weak fibrant replacement you only add fillers for > some of these lifting problems. The pushout product of a monomorphism A -> B > with endpoint inclusion always has codomain B x I - then only consider those > lifting problems where the bottom map factors through the projection B x I > -> B. I think there are two ways to ensure that the operation of weak > fibrant replacement is stable under pullback - one way is carry out the > operation "internally" in simplicial sets (viewed as a topos), and the other > to use the algebraic small object argument, ensuring that uniformity > condition above is in the definition. The intuitive reason why this should > be stable is that the problem that stops the usual fibrant replacement from > being stable is that e.g. when we freely add the transport of a point along > a path, p we are adding a new element to the fibre of p(1) which depends on > things outside of that fibre, whereas with weak fibrant replacement we only > add a filler to an open box to a certain fibre if the original open box lies > entirely in that fibre. > > In order to show that the suspension is fibrant one has to use both the > structure already present in pre suspension (transport and flattening) and > the additional structure added by weak fibrant replacement. The idea is to > follow the same proof as for cubical type theory. It is enough to just show > composition and then derive filling. So to define the composition of an open > box, first flatten it, then use the weak fibration structure to find the > composition. (And I think that last part should be an instance of a general > result along the lines of "if the monad of transport and flattening > distributes over a monad, then the fibrant replacement monad distributes > over the coproduct of that monad with weak fibrant replacement"). > > > Best, > Andrew > > > On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: >> >> On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine >> <p.l....@gmail.com> 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. >> >> >> I realise I was a bit unclear here: it’s only suspension that I meant to >> suggest is problematic, not propositional truncation. The latter seems a >> bit easier to do by ad hoc constructions; e.g. the construction below does >> it in simplicial sets, and I think a similar thing may work also in cubical >> sets. (I don’t claim originality for this construction; I don’t think I >> learned it from anywhere, but I do recall discussing it with people who were >> already aware of it or something similar (I think at least Mike, Thierry, >> and Simon Huber, at various times?), so I think multiple people may have >> noticed it independently.) >> >> So suspension (or more generally pushouts/coequalisers) is what would make >> a really good test case for any proposed general approach — it’s the >> simplest HIT which as far as I know hasn’t been modelled without a size >> blowup in any infinite-dimensional model except cubical sets, under any of >> the approaches to modelling HIT’s proposed so far. (Am I right in >> remembering that this has been given for cubical sets? I can’t find it in >> any of the writeups, but I seem to recall hearing it presented at >> conferences.) >> >> Construction of propositional truncation without size blowup in simplicial >> sets: >> >> (1) Given a fibration Y —> X, define |Y| —> X as follows: >> >> an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with >> a “partial lift of x into Y, defined at least on all vertices”, i.e. a >> subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that >> the evident square commutes; >> >> reindexing acts by taking pullbacks/inverse images of the domain of the >> partial lift (i.e. the usual composition of a partial map with a total map). >> >> (2) There’s an evident map Y —> |Y| over X; and the operation sending Y to >> Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X. >> (Straightforward.) >> >> (3) In general, a fibration is a proposition in the type-theoretic sense >> iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. >> (Non-trivial but not too hard to check.) >> >> (4) The map |Y| —> X is a fibration, and a proposition. (Straightforward, >> given (3), by concretely constructing the required liftings.) >> >> (5) The evident map Y —> |Y| over X is a cell complex constructed from >> boundary inclusions δ[n] —> Δ[n] with n > 0. >> >> To see this: take the filtration of |Y| by subobjects Y_n, where the >> non-degenerate simplices of Y_n are those whose “missing” simplices are all >> of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} >> that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the >> inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> >> Δ[n+1]. >> >> (6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably >> in X. (Orthogonality is immediate from (3) and (5); stability is then by >> (2).) >> >> (7) Let V be either the universe of “well-ordered α-small fibrations”, or >> the universe of “displayed α-small fibrations”, for α any infinite regular >> cardinal. Then V carries an operation representing the construction of (1), >> and modelling propositional truncation. (Lengthy to spell out in full, but >> straightforward given (2), (6).) >> >> >> –p. >> >> >> > -- > 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. ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-07 23:06 ` Michael Shulman @ 2017-06-08 6:35 ` Andrew Swan 0 siblings, 0 replies; 25+ messages in thread From: Andrew Swan @ 2017-06-08 6:35 UTC (permalink / raw) To: Homotopy Type Theory; +Cc: wakeli..., awo..., Thierry... [-- Attachment #1.1: Type: text/plain, Size: 717 bytes --] > > Why is there no LOG in this? It's a little messy to write out the actual details, but it is possible for each map f : X -> Y to use the subobject classifier and dependent products to construct a "universal lifting problem" for f, where universal means that every other lifting problem against a pushout product of monomorphism and i-endpoint inclusion factors uniquely as a pullback followed by the universal lifting problem. Then, once a filler for the universal lifting problem has been chosen, it can be used to construct a filler for all the other lifting problems. (This can also be seen as an instance of a general result that holds in any locally small fibration with finitely complete base). [-- Attachment #1.2: Type: text/html, Size: 906 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> 2017-06-07 23:06 ` Michael Shulman @ 2018-09-14 11:15 ` Thierry Coquand 2018-09-14 14:16 ` Andrew Swan 1 sibling, 1 reply; 25+ messages in thread From: Thierry Coquand @ 2018-09-14 11:15 UTC (permalink / raw) To: HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 9028 bytes --] I wrote a short note<http://www.cse.chalmers.se/~coquand/hits.pdf> to confirm Andrew’s message that indeed this technique works as well (using classical logic) for simplicial sets. This can now be presented as a combination of various published results. (The originality is only in the presentation; this essentially follows what is suggested in Andrew’s message.) This provides a semantics of e.g. suspension as an operation U -> U, where U is an univalent universe in the simplicial set model. Thierry On 7 Jun 2017, at 14:34, Andrew Swan <wakelin.swan@gmail.com<mailto:wakelin.swan@gmail.com>> wrote: So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) The technique used in cubical type theory seems fairly flexible. I'm not sure exactly how flexible, but I think I can get suspension to work in simplicial sets. In the below, throughout I use the characterisation of fibrations as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the interval. WLOG there is also a uniformity condition - we have a choice of lift and "pulling back the monomorphism preserves the lift." Given a fibration X -> Y, you first freely add elements N and S together with a path from N to S for each element of X (I think this is the same as what you called pre suspension). Although the pre suspension is not a fibration in general, it does have some of the properties you might expect from a fibration. Given a path in Y, and an element in the fibre of an endpoint, one can transport along the path to get something in the fibre of the other endpoint. There should also be a "flattening" operation that takes a path q in presuspension(X) over p in Y, and returns a path from q(1) to the transport along p of q(0) that lies entirely in the fibre of p(1). You then take the "weak fibrant replacement" of the pre suspension. A map in simplicial sets is a fibration if and only if it has the rlp against each pushout product of a monomorphism with an endpoint inclusion into the interval. In fibrant replacement you freely add a diagonal lift for each such lifting problems. In weak fibrant replacement you only add fillers for some of these lifting problems. The pushout product of a monomorphism A -> B with endpoint inclusion always has codomain B x I - then only consider those lifting problems where the bottom map factors through the projection B x I -> B. I think there are two ways to ensure that the operation of weak fibrant replacement is stable under pullback - one way is carry out the operation "internally" in simplicial sets (viewed as a topos), and the other to use the algebraic small object argument, ensuring that uniformity condition above is in the definition. The intuitive reason why this should be stable is that the problem that stops the usual fibrant replacement from being stable is that e.g. when we freely add the transport of a point along a path, p we are adding a new element to the fibre of p(1) which depends on things outside of that fibre, whereas with weak fibrant replacement we only add a filler to an open box to a certain fibre if the original open box lies entirely in that fibre. In order to show that the suspension is fibrant one has to use both the structure already present in pre suspension (transport and flattening) and the additional structure added by weak fibrant replacement. The idea is to follow the same proof as for cubical type theory. It is enough to just show composition and then derive filling. So to define the composition of an open box, first flatten it, then use the weak fibration structure to find the composition. (And I think that last part should be an instance of a general result along the lines of "if the monad of transport and flattening distributes over a monad, then the fibrant replacement monad distributes over the coproduct of that monad with weak fibrant replacement"). Best, Andrew On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> 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. I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.) So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) Construction of propositional truncation without size blowup in simplicial sets: (1) Given a fibration Y —> X, define |Y| —> X as follows: an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with a “partial lift of x into Y, defined at least on all vertices”, i.e. a subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that the evident square commutes; reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map). (2) There’s an evident map Y —> |Y| over X; and the operation sending Y to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X. (Straightforward.) (3) In general, a fibration is a proposition in the type-theoretic sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. (Non-trivial but not too hard to check.) (4) The map |Y| —> X is a fibration, and a proposition. (Straightforward, given (3), by concretely constructing the required liftings.) (5) The evident map Y —> |Y| over X is a cell complex constructed from boundary inclusions δ[n] —> Δ[n] with n > 0. To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose “missing” simplices are all of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> Δ[n+1]. (6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably in X. (Orthogonality is immediate from (3) and (5); stability is then by (2).) (7) Let V be either the universe of “well-ordered α-small fibrations”, or the universe of “displayed α-small fibrations”, for α any infinite regular cardinal. Then V carries an operation representing the construction of (1), and modelling propositional truncation. (Lengthy to spell out in full, but straightforward given (2), (6).) –p. -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 12412 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2018-09-14 11:15 ` Thierry Coquand @ 2018-09-14 14:16 ` Andrew Swan 2018-10-01 13:02 ` Thierry Coquand 0 siblings, 1 reply; 25+ messages in thread From: Andrew Swan @ 2018-09-14 14:16 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 11988 bytes --] Thanks for writing out the note. I'll also make a few remarks about how my more recent work connects with these things. 1. The initial Susp X algebras, and I think in fact all of the initial algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed by combining finite colimits and W types with reductions (as appearing in this paper <https://arxiv.org/abs/1802.07588>). From this it follows that they exist not just in cubical sets and simplicial sets, but any topos that satisfies WISC, and for the special case of presheaf categories with locally decidable cofibrations they can be constructed without using WISC or exact quotients. I think the latter can be viewed as a generalisation of the Coquand-Huber-Mortberg definition. 2. In my post and again in the W-types with reductions paper I suggested using Christian's generalised notion of lifting property for commutative squares. I still think this works, but I now lean towards other ways of looking at it. I didn't really emphasise this in the paper, but it follows from the general theory that one obtains not just an awfs, but a fibred awfs over the codomain fibration. This gives an awfs, and thereby a notion of trivial cofibration and fibration for each slice category C/Y. Then given a map f : X -> Y, we can either view it as a map in the slice category C/1 and factorise it there or as a map into the terminal object in the slice category C/Y. The latter is necessarily stable under pullback, and I think works out the same as "freely adding a homogeneous filling operator." Alternatively, it is also possible to use W types with reductions directly, without going via the small object argument. In this case the proofs in the Coquand-Huber-Mortberg paper generalise pretty much directly with very little modification. 3. I still find the situation in simplicial sets a little strange, in particular the need to switch back and forth between the different notions of fibration, although it does work as far as I can tell. 4. I made some remarks before about universal lifting problems. These now appear in the paper Lifting Problems in Grothendieck Fibrations <https://arxiv.org/abs/1802.06718> . Best, Andrew On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: > > > I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> to > confirm Andrew’s message that indeed this technique > works as well (using classical logic) for simplicial sets. This can now be > presented > as a combination of various published results. (The originality is only in > the presentation; > this essentially follows what is suggested in Andrew’s message.) > This provides a semantics of e.g. suspension as an operation U -> U, > where U > is an univalent universe in the simplicial set model. > > Thierry > > > On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com <javascript:>> > wrote: > > So suspension (or more generally pushouts/coequalisers) is what would make >> a really good test case for any proposed general approach — it’s the >> simplest HIT which as far as I know hasn’t been modelled without a size >> blowup in any infinite-dimensional model except cubical sets, under any of >> the approaches to modelling HIT’s proposed so far. (Am I right in >> remembering that this has been given for cubical sets? I can’t find it in >> any of the writeups, but I seem to recall hearing it presented at >> conferences.) > > > The technique used in cubical type theory seems fairly flexible. I'm not > sure exactly how flexible, but I think I can get suspension to work in > simplicial sets. In the below, throughout I use the characterisation of > fibrations as maps with the rlp against the pushout product of each > monomorphism with endpoint inclusion into the interval. WLOG there is also > a uniformity condition - we have a choice of lift and "pulling back the > monomorphism preserves the lift." > > Given a fibration X -> Y, you first freely add elements N and S together > with a path from N to S for each element of X (I think this is the same as > what you called pre suspension). Although the pre suspension is not a > fibration in general, it does have some of the properties you might expect > from a fibration. Given a path in Y, and an element in the fibre of an > endpoint, one can transport along the path to get something in the fibre of > the other endpoint. There should also be a "flattening" operation that > takes a path q in presuspension(X) over p in Y, and returns a path from > q(1) to the transport along p of q(0) that lies entirely in the fibre of > p(1). > > You then take the "weak fibrant replacement" of the pre suspension. A map > in simplicial sets is a fibration if and only if it has the rlp against > each pushout product of a monomorphism with an endpoint inclusion into the > interval. In fibrant replacement you freely add a diagonal lift for each > such lifting problems. In weak fibrant replacement you only add fillers for > some of these lifting problems. The pushout product of a monomorphism A -> > B with endpoint inclusion always has codomain B x I - then only consider > those lifting problems where the bottom map factors through the projection > B x I -> B. I think there are two ways to ensure that the operation of weak > fibrant replacement is stable under pullback - one way is carry out the > operation "internally" in simplicial sets (viewed as a topos), and the > other to use the algebraic small object argument, ensuring that uniformity > condition above is in the definition. The intuitive reason why this should > be stable is that the problem that stops the usual fibrant replacement from > being stable is that e.g. when we freely add the transport of a point along > a path, p we are adding a new element to the fibre of p(1) which depends on > things outside of that fibre, whereas with weak fibrant replacement we only > add a filler to an open box to a certain fibre if the original open box > lies entirely in that fibre. > > In order to show that the suspension is fibrant one has to use both the > structure already present in pre suspension (transport and flattening) and > the additional structure added by weak fibrant replacement. The idea is to > follow the same proof as for cubical type theory. It is enough to just show > composition and then derive filling. So to define the composition of an > open box, first flatten it, then use the weak fibration structure to find > the composition. (And I think that last part should be an instance of a > general result along the lines of "if the monad of transport and flattening > distributes over a monad, then the fibrant replacement monad distributes > over the coproduct of that monad with weak fibrant replacement"). > > > Best, > Andrew > > > On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: >> >> On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine < >> p.l.lu...@gmail.com> 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. >>> >> >> I realise I was a bit unclear here: it’s only suspension that I meant to >> suggest is problematic, not propositional truncation. The latter seems a >> bit easier to do by ad hoc constructions; e.g. the construction below does >> it in simplicial sets, and I think a similar thing may work also in cubical >> sets. (I don’t claim originality for this construction; I don’t think I >> learned it from anywhere, but I do recall discussing it with people who >> were already aware of it or something similar (I think at least Mike, >> Thierry, and Simon Huber, at various times?), so I think multiple people >> may have noticed it independently.) >> >> So suspension (or more generally pushouts/coequalisers) is what would >> make a really good test case for any proposed general approach — it’s the >> simplest HIT which as far as I know hasn’t been modelled without a size >> blowup in any infinite-dimensional model except cubical sets, under any of >> the approaches to modelling HIT’s proposed so far. (Am I right in >> remembering that this has been given for cubical sets? I can’t find it in >> any of the writeups, but I seem to recall hearing it presented at >> conferences.) >> >> Construction of propositional truncation without size blowup in >> simplicial sets: >> >> (1) Given a fibration Y —> X, define |Y| —> X as follows: >> >> an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with >> a “partial lift of x into Y, defined at least on all vertices”, i.e. a >> subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such >> that the evident square commutes; >> >> reindexing acts by taking pullbacks/inverse images of the domain of the >> partial lift (i.e. the usual composition of a partial map with a total map). >> >> (2) There’s an evident map Y —> |Y| over X; and the operation sending Y >> to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in >> X. (Straightforward.) >> >> (3) In general, a fibration is a proposition in the type-theoretic sense >> iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. >> (Non-trivial but not too hard to check.) >> >> (4) The map |Y| —> X is a fibration, and a proposition. >> (Straightforward, given (3), by concretely constructing the required >> liftings.) >> >> (5) The evident map Y —> |Y| over X is a cell complex constructed from >> boundary inclusions δ[n] —> Δ[n] with n > 0. >> >> To see this: take the filtration of |Y| by subobjects Y_n, where the >> non-degenerate simplices of Y_n are those whose “missing” simplices are all >> of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} >> that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the >> inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> >> Δ[n+1]. >> >> (6) The map Y —> |Y| is orthogonal to all propositional fibrations, >> stably in X. (Orthogonality is immediate from (3) and (5); stability is >> then by (2).) >> >> (7) Let V be either the universe of “well-ordered α-small fibrations”, or >> the universe of “displayed α-small fibrations”, for α any infinite regular >> cardinal. Then V carries an operation representing the construction of >> (1), and modelling propositional truncation. (Lengthy to spell out in >> full, but straightforward given (2), (6).) >> >> >> –p. >> >> >> >> > -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 14273 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2018-09-14 14:16 ` Andrew Swan @ 2018-10-01 13:02 ` Thierry Coquand 2018-11-10 15:52 ` Anders Mörtberg 0 siblings, 1 reply; 25+ messages in thread From: Thierry Coquand @ 2018-10-01 13:02 UTC (permalink / raw) To: Andrew Swan; +Cc: Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 13547 bytes --] Following the previous note on semantics of HIT in the simplicial set model, I looked a little more at the formal system which is similar to cubical type theory (based on distributive lattices) but where the filling operation is treated as a -constant- (without any computation rule). This formal system has models in simplicial and cubical sets. It is possible to show for this system a canonicity theorem, similar to Voevodsky’s conjecture: a closed term of type Bool is -path equal- to 0 or 1. (With a similar statement for natural numbers.) A corollary of this result is that the value of such a closed term is the same in all models. Hence we know that the computation of such a closed term in various extensions where we can compute the filling operation will give the same value (and the same value which we get in simplicial set; so e.g. Brunerie constant has to be +/-2 in the model based on de Morgan algebras). This is proved using the sconing technique as described in https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html As is stated there, the problem for using this technique to solve Voevodsky’s conjecture is that there s no apparent way to associate (in a “strict” way) a simplicial/cubical set to a closed type in dependent type theory with identity types. This issue disappears here thanks to the use of higher dimensional syntax. I wrote a proof <http://www.cse.chalmers.se/~coquand/can3.pdf> which is the result of several discussions with Simon Huber and Christian Sattler on this topic. The proof can be done effectively using the cubical set model, or non effectively using the simplicial set model. Maybe a similar result can be proved for simplicial/cubical tribes. Thierry On 14 Sep 2018, at 16:16, Andrew Swan <wakelin.swan@gmail.com<mailto:wakelin.swan@gmail.com>> wrote: Thanks for writing out the note. I'll also make a few remarks about how my more recent work connects with these things. 1. The initial Susp X algebras, and I think in fact all of the initial algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed by combining finite colimits and W types with reductions (as appearing in this paper<https://arxiv.org/abs/1802.07588>). From this it follows that they exist not just in cubical sets and simplicial sets, but any topos that satisfies WISC, and for the special case of presheaf categories with locally decidable cofibrations they can be constructed without using WISC or exact quotients. I think the latter can be viewed as a generalisation of the Coquand-Huber-Mortberg definition. 2. In my post and again in the W-types with reductions paper I suggested using Christian's generalised notion of lifting property for commutative squares. I still think this works, but I now lean towards other ways of looking at it. I didn't really emphasise this in the paper, but it follows from the general theory that one obtains not just an awfs, but a fibred awfs over the codomain fibration. This gives an awfs, and thereby a notion of trivial cofibration and fibration for each slice category C/Y. Then given a map f : X -> Y, we can either view it as a map in the slice category C/1 and factorise it there or as a map into the terminal object in the slice category C/Y. The latter is necessarily stable under pullback, and I think works out the same as "freely adding a homogeneous filling operator." Alternatively, it is also possible to use W types with reductions directly, without going via the small object argument. In this case the proofs in the Coquand-Huber-Mortberg paper generalise pretty much directly with very little modification. 3. I still find the situation in simplicial sets a little strange, in particular the need to switch back and forth between the different notions of fibration, although it does work as far as I can tell. 4. I made some remarks before about universal lifting problems. These now appear in the paper Lifting Problems in Grothendieck Fibrations<https://arxiv.org/abs/1802.06718> . Best, Andrew On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: I wrote a short note<http://www.cse.chalmers.se/~coquand/hits.pdf> to confirm Andrew’s message that indeed this technique works as well (using classical logic) for simplicial sets. This can now be presented as a combination of various published results. (The originality is only in the presentation; this essentially follows what is suggested in Andrew’s message.) This provides a semantics of e.g. suspension as an operation U -> U, where U is an univalent universe in the simplicial set model. Thierry On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com<http://gmail.com/>> wrote: So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) The technique used in cubical type theory seems fairly flexible. I'm not sure exactly how flexible, but I think I can get suspension to work in simplicial sets. In the below, throughout I use the characterisation of fibrations as maps with the rlp against the pushout product of each monomorphism with endpoint inclusion into the interval. WLOG there is also a uniformity condition - we have a choice of lift and "pulling back the monomorphism preserves the lift." Given a fibration X -> Y, you first freely add elements N and S together with a path from N to S for each element of X (I think this is the same as what you called pre suspension). Although the pre suspension is not a fibration in general, it does have some of the properties you might expect from a fibration. Given a path in Y, and an element in the fibre of an endpoint, one can transport along the path to get something in the fibre of the other endpoint. There should also be a "flattening" operation that takes a path q in presuspension(X) over p in Y, and returns a path from q(1) to the transport along p of q(0) that lies entirely in the fibre of p(1). You then take the "weak fibrant replacement" of the pre suspension. A map in simplicial sets is a fibration if and only if it has the rlp against each pushout product of a monomorphism with an endpoint inclusion into the interval. In fibrant replacement you freely add a diagonal lift for each such lifting problems. In weak fibrant replacement you only add fillers for some of these lifting problems. The pushout product of a monomorphism A -> B with endpoint inclusion always has codomain B x I - then only consider those lifting problems where the bottom map factors through the projection B x I -> B. I think there are two ways to ensure that the operation of weak fibrant replacement is stable under pullback - one way is carry out the operation "internally" in simplicial sets (viewed as a topos), and the other to use the algebraic small object argument, ensuring that uniformity condition above is in the definition. The intuitive reason why this should be stable is that the problem that stops the usual fibrant replacement from being stable is that e.g. when we freely add the transport of a point along a path, p we are adding a new element to the fibre of p(1) which depends on things outside of that fibre, whereas with weak fibrant replacement we only add a filler to an open box to a certain fibre if the original open box lies entirely in that fibre. In order to show that the suspension is fibrant one has to use both the structure already present in pre suspension (transport and flattening) and the additional structure added by weak fibrant replacement. The idea is to follow the same proof as for cubical type theory. It is enough to just show composition and then derive filling. So to define the composition of an open box, first flatten it, then use the weak fibration structure to find the composition. (And I think that last part should be an instance of a general result along the lines of "if the monad of transport and flattening distributes over a monad, then the fibrant replacement monad distributes over the coproduct of that monad with weak fibrant replacement"). Best, Andrew On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> 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. I realise I was a bit unclear here: it’s only suspension that I meant to suggest is problematic, not propositional truncation. The latter seems a bit easier to do by ad hoc constructions; e.g. the construction below does it in simplicial sets, and I think a similar thing may work also in cubical sets. (I don’t claim originality for this construction; I don’t think I learned it from anywhere, but I do recall discussing it with people who were already aware of it or something similar (I think at least Mike, Thierry, and Simon Huber, at various times?), so I think multiple people may have noticed it independently.) So suspension (or more generally pushouts/coequalisers) is what would make a really good test case for any proposed general approach — it’s the simplest HIT which as far as I know hasn’t been modelled without a size blowup in any infinite-dimensional model except cubical sets, under any of the approaches to modelling HIT’s proposed so far. (Am I right in remembering that this has been given for cubical sets? I can’t find it in any of the writeups, but I seem to recall hearing it presented at conferences.) Construction of propositional truncation without size blowup in simplicial sets: (1) Given a fibration Y —> X, define |Y| —> X as follows: an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together with a “partial lift of x into Y, defined at least on all vertices”, i.e. a subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such that the evident square commutes; reindexing acts by taking pullbacks/inverse images of the domain of the partial lift (i.e. the usual composition of a partial map with a total map). (2) There’s an evident map Y —> |Y| over X; and the operation sending Y to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in X. (Straightforward.) (3) In general, a fibration is a proposition in the type-theoretic sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. (Non-trivial but not too hard to check.) (4) The map |Y| —> X is a fibration, and a proposition. (Straightforward, given (3), by concretely constructing the required liftings.) (5) The evident map Y —> |Y| over X is a cell complex constructed from boundary inclusions δ[n] —> Δ[n] with n > 0. To see this: take the filtration of |Y| by subobjects Y_n, where the non-degenerate simplices of Y_n are those whose “missing” simplices are all of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> Δ[n+1]. (6) The map Y —> |Y| is orthogonal to all propositional fibrations, stably in X. (Orthogonality is immediate from (3) and (5); stability is then by (2).) (7) Let V be either the universe of “well-ordered α-small fibrations”, or the universe of “displayed α-small fibrations”, for α any infinite regular cardinal. Then V carries an operation representing the construction of (1), and modelling propositional truncation. (Lengthy to spell out in full, but straightforward given (2), (6).) –p. -- 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+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 24085 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2018-10-01 13:02 ` Thierry Coquand @ 2018-11-10 15:52 ` Anders Mörtberg 2018-11-10 18:21 ` Gabriel Scherer 0 siblings, 1 reply; 25+ messages in thread From: Anders Mörtberg @ 2018-11-10 15:52 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 17255 bytes --] This is very exciting! Around the time when Thierry sent his message I did a little experiment where I made comp compute to a value in cubicaltt (this means that it is not defined by cases on the type as in the CCHM paper): https://github.com/mortberg/cubicaltt/tree/compval What I then realized was that the full proof of univalence (using that unglue is an equivalence) goes through as it is: https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L330 The same holds for the proof of univalence using Id everywhere. This was a bit surprising to me at first as it shows that none of the computation rules for comp by case on the type matter in these proofs (note that we still have the equations for how "comp^i A [phi -> u] u0" computes under phi : FF). However some proofs did of course break, for example the direct proof of "uabeta" which relies on how comp in Glue computes in the CCHM cubical set model. So it seems to me like the system that Thierry describes in his message has many very good properties that have been missing or are unknown from the proposed type theories for univalent type theory so far, in particular: - It has a model in Kan simplicial sets and a constructive model in ("Dedekind"/distributive lattice) cubical sets - It satisfies homotopy canonicity so that we know that all terms of type nat "compute" to the same numerals in these models - It has Id types (with strict computation for J) and univalence is a theorem for these types - As comp doesn't compute the implementation of the type theory is much simpler and type checking is very fast compared to regular cubicaltt The only downside is that it doesn't have "strict" canonicity (not all closed terms of type nat are judgmentally equal to a numeral), but I don't think that this is too much of a problem in practice as we can implement a closed term evaluator inspired by the cubical set model for computing these numerals (much like how Coq has vm/native_compute for efficient computation of closed terms). Finally my little experiment indicates that having a comp which doesn't compute doesn't affect the practical usability of this system too much either. -- Anders PS: Note that I didn't remove reversals in my small experiment as it would require a bit more hacking and I didn't have time to do it, but there is no fundamental problem in doing this and from my experience with cartesian cubical type theory it is not too bad in practice either (we would drop reversals and instead have comp 0->1 and comp 1->0). On Monday, October 1, 2018 at 9:02:53 AM UTC-4, coquand wrote: > > Following the previous note on semantics of HIT in the simplicial set > model, I looked > a little more at the formal system which is similar to cubical type theory > (based on distributive > lattices) but where the filling operation is treated as a -constant- > (without any computation rule). > > This formal system has models in simplicial and cubical sets. > > It is possible to show for this system a canonicity theorem, similar to > Voevodsky’s conjecture: a closed > term of type Bool is -path equal- to 0 or 1. (With a similar statement for > natural numbers.) > > A corollary of this result is that the value of such a closed term is the > same in all models. Hence > we know that the computation of such a closed term in various extensions > where we can compute > the filling operation will give the same value (and the same value which > we get in simplicial set; so e.g. > Brunerie constant has to be +/-2 in the model based on de Morgan algebras). > > This is proved using the sconing technique as described in > > > https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html > > As is stated there, the problem for using this technique to solve > Voevodsky’s conjecture is that there > s no apparent way to associate (in a “strict” way) a simplicial/cubical > set to a closed type in dependent > type theory with identity types. > > This issue disappears here thanks to the use of higher dimensional syntax. > > I wrote a proof <http://www.cse.chalmers.se/~coquand/can3.pdf>which is > the result of several discussions with Simon Huber and Christian Sattler > on this topic. The proof can be done effectively using the cubical set > model, or non effectively using the simplicial > set model. > Maybe a similar result can be proved for simplicial/cubical tribes. > > Thierry > > > On 14 Sep 2018, at 16:16, Andrew Swan <wakeli...@gmail.com <javascript:>> > wrote: > > Thanks for writing out the note. I'll also make a few remarks about how my > more recent work connects with these things. > > 1. The initial Susp X algebras, and I think in fact all of the initial > algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed > by combining finite colimits and W types with reductions (as appearing in this > paper <https://arxiv.org/abs/1802.07588>). From this it follows that they > exist not just in cubical sets and simplicial sets, but any topos that > satisfies WISC, and for the special case of presheaf categories with > locally decidable cofibrations they can be constructed without using WISC > or exact quotients. I think the latter can be viewed as a generalisation of > the Coquand-Huber-Mortberg definition. > > 2. In my post and again in the W-types with reductions paper I suggested > using Christian's generalised notion of lifting property for commutative > squares. I still think this works, but I now lean towards other ways of > looking at it. I didn't really emphasise this in the paper, but it follows > from the general theory that one obtains not just an awfs, but a fibred > awfs over the codomain fibration. This gives an awfs, and thereby a notion > of trivial cofibration and fibration for each slice category C/Y. Then > given a map f : X -> Y, we can either view it as a map in the slice > category C/1 and factorise it there or as a map into the terminal object in > the slice category C/Y. The latter is necessarily stable under pullback, > and I think works out the same as "freely adding a homogeneous filling > operator." > > Alternatively, it is also possible to use W types with reductions > directly, without going via the small object argument. In this case the > proofs in the Coquand-Huber-Mortberg paper generalise pretty much directly > with very little modification. > > 3. I still find the situation in simplicial sets a little strange, in > particular the need to switch back and forth between the different notions > of fibration, although it does work as far as I can tell. > > 4. I made some remarks before about universal lifting problems. These now > appear in the paper Lifting Problems in Grothendieck Fibrations > <https://arxiv.org/abs/1802.06718> . > > Best, > Andrew > > > On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: >> >> >> I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> to >> confirm Andrew’s message that indeed this technique >> works as well (using classical logic) for simplicial sets. This can now >> be presented >> as a combination of various published results. (The originality is only >> in the presentation; >> this essentially follows what is suggested in Andrew’s message.) >> This provides a semantics of e.g. suspension as an operation U -> U, >> where U >> is an univalent universe in the simplicial set model. >> >> Thierry >> >> >> On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com> wrote: >> >> So suspension (or more generally pushouts/coequalisers) is what would >>> make a really good test case for any proposed general approach — it’s the >>> simplest HIT which as far as I know hasn’t been modelled without a size >>> blowup in any infinite-dimensional model except cubical sets, under any of >>> the approaches to modelling HIT’s proposed so far. (Am I right in >>> remembering that this has been given for cubical sets? I can’t find it in >>> any of the writeups, but I seem to recall hearing it presented at >>> conferences.) >> >> >> The technique used in cubical type theory seems fairly flexible. I'm not >> sure exactly how flexible, but I think I can get suspension to work in >> simplicial sets. In the below, throughout I use the characterisation of >> fibrations as maps with the rlp against the pushout product of each >> monomorphism with endpoint inclusion into the interval. WLOG there is also >> a uniformity condition - we have a choice of lift and "pulling back the >> monomorphism preserves the lift." >> >> Given a fibration X -> Y, you first freely add elements N and S together >> with a path from N to S for each element of X (I think this is the same as >> what you called pre suspension). Although the pre suspension is not a >> fibration in general, it does have some of the properties you might expect >> from a fibration. Given a path in Y, and an element in the fibre of an >> endpoint, one can transport along the path to get something in the fibre of >> the other endpoint. There should also be a "flattening" operation that >> takes a path q in presuspension(X) over p in Y, and returns a path from >> q(1) to the transport along p of q(0) that lies entirely in the fibre of >> p(1). >> >> You then take the "weak fibrant replacement" of the pre suspension. A >> map in simplicial sets is a fibration if and only if it has the rlp against >> each pushout product of a monomorphism with an endpoint inclusion into the >> interval. In fibrant replacement you freely add a diagonal lift for each >> such lifting problems. In weak fibrant replacement you only add fillers for >> some of these lifting problems. The pushout product of a monomorphism A -> >> B with endpoint inclusion always has codomain B x I - then only consider >> those lifting problems where the bottom map factors through the projection >> B x I -> B. I think there are two ways to ensure that the operation of weak >> fibrant replacement is stable under pullback - one way is carry out the >> operation "internally" in simplicial sets (viewed as a topos), and the >> other to use the algebraic small object argument, ensuring that uniformity >> condition above is in the definition. The intuitive reason why this should >> be stable is that the problem that stops the usual fibrant replacement from >> being stable is that e.g. when we freely add the transport of a point along >> a path, p we are adding a new element to the fibre of p(1) which depends on >> things outside of that fibre, whereas with weak fibrant replacement we only >> add a filler to an open box to a certain fibre if the original open box >> lies entirely in that fibre. >> >> In order to show that the suspension is fibrant one has to use both the >> structure already present in pre suspension (transport and flattening) and >> the additional structure added by weak fibrant replacement. The idea is to >> follow the same proof as for cubical type theory. It is enough to just show >> composition and then derive filling. So to define the composition of an >> open box, first flatten it, then use the weak fibration structure to find >> the composition. (And I think that last part should be an instance of a >> general result along the lines of "if the monad of transport and flattening >> distributes over a monad, then the fibrant replacement monad distributes >> over the coproduct of that monad with weak fibrant replacement"). >> >> >> Best, >> Andrew >> >> >> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: >>> >>> On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine < >>> p.l.lu...@gmail.com> 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. >>>> >>> >>> I realise I was a bit unclear here: it’s only suspension that I meant to >>> suggest is problematic, not propositional truncation. The latter seems a >>> bit easier to do by ad hoc constructions; e.g. the construction below does >>> it in simplicial sets, and I think a similar thing may work also in cubical >>> sets. (I don’t claim originality for this construction; I don’t think I >>> learned it from anywhere, but I do recall discussing it with people who >>> were already aware of it or something similar (I think at least Mike, >>> Thierry, and Simon Huber, at various times?), so I think multiple people >>> may have noticed it independently.) >>> >>> So suspension (or more generally pushouts/coequalisers) is what would >>> make a really good test case for any proposed general approach — it’s the >>> simplest HIT which as far as I know hasn’t been modelled without a size >>> blowup in any infinite-dimensional model except cubical sets, under any of >>> the approaches to modelling HIT’s proposed so far. (Am I right in >>> remembering that this has been given for cubical sets? I can’t find it in >>> any of the writeups, but I seem to recall hearing it presented at >>> conferences.) >>> >>> Construction of propositional truncation without size blowup in >>> simplicial sets: >>> >>> (1) Given a fibration Y —> X, define |Y| —> X as follows: >>> >>> an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together >>> with a “partial lift of x into Y, defined at least on all vertices”, i.e. a >>> subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such >>> that the evident square commutes; >>> >>> reindexing acts by taking pullbacks/inverse images of the domain of the >>> partial lift (i.e. the usual composition of a partial map with a total map). >>> >>> (2) There’s an evident map Y —> |Y| over X; and the operation sending Y >>> to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in >>> X. (Straightforward.) >>> >>> (3) In general, a fibration is a proposition in the type-theoretic sense >>> iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n > 0. >>> (Non-trivial but not too hard to check.) >>> >>> (4) The map |Y| —> X is a fibration, and a proposition. >>> (Straightforward, given (3), by concretely constructing the required >>> liftings.) >>> >>> (5) The evident map Y —> |Y| over X is a cell complex constructed from >>> boundary inclusions δ[n] —> Δ[n] with n > 0. >>> >>> To see this: take the filtration of |Y| by subobjects Y_n, where the >>> non-degenerate simplices of Y_n are those whose “missing” simplices are all >>> of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} >>> that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the >>> inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> >>> Δ[n+1]. >>> >>> (6) The map Y —> |Y| is orthogonal to all propositional fibrations, >>> stably in X. (Orthogonality is immediate from (3) and (5); stability is >>> then by (2).) >>> >>> (7) Let V be either the universe of “well-ordered α-small fibrations”, >>> or the universe of “displayed α-small fibrations”, for α any infinite >>> regular cardinal. Then V carries an operation representing the >>> construction of (1), and modelling propositional truncation. (Lengthy to >>> spell out in full, but straightforward given (2), (6).) >>> >>> >>> –p. >>> >>> >>> >>> >> > -- > 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+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 26226 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2018-11-10 15:52 ` Anders Mörtberg @ 2018-11-10 18:21 ` Gabriel Scherer 0 siblings, 0 replies; 25+ messages in thread From: Gabriel Scherer @ 2018-11-10 18:21 UTC (permalink / raw) To: andersmortberg; +Cc: HomotopyTypeTheory [-- Attachment #1: Type: text/plain, Size: 18150 bytes --] I wouldn't compare your proposal (if I understand it correctly) with vm_compute and native_compute, which only make reductions that are valid for Coq's beta-reduction. They are implemented differently and reduce terms in different ways, but they must not change the theory of equality of the system. On Sat, Nov 10, 2018 at 4:52 PM Anders Mörtberg <andersmortberg@gmail.com> wrote: > This is very exciting! > > Around the time when Thierry sent his message I did a little experiment > where I made comp compute to a value in cubicaltt (this means that it is > not defined by cases on the type as in the CCHM paper): > > https://github.com/mortberg/cubicaltt/tree/compval > > What I then realized was that the full proof of univalence (using that > unglue is an equivalence) goes through as it is: > > > https://github.com/mortberg/cubicaltt/blob/compval/examples/compval.ctt#L330 > > The same holds for the proof of univalence using Id everywhere. This was a > bit surprising to me at first as it shows that none of the computation > rules for comp by case on the type matter in these proofs (note that we > still have the equations for how "comp^i A [phi -> u] u0" computes under > phi : FF). However some proofs did of course break, for example the direct > proof of "uabeta" which relies on how comp in Glue computes in the CCHM > cubical set model. > > > So it seems to me like the system that Thierry describes in his message > has many very good properties that have been missing or are unknown from > the proposed type theories for univalent type theory so far, in particular: > > - It has a model in Kan simplicial sets and a constructive model in > ("Dedekind"/distributive lattice) cubical sets > > - It satisfies homotopy canonicity so that we know that all terms of type > nat "compute" to the same numerals in these models > > - It has Id types (with strict computation for J) and univalence is a > theorem for these types > > - As comp doesn't compute the implementation of the type theory is much > simpler and type checking is very fast compared to regular cubicaltt > > > The only downside is that it doesn't have "strict" canonicity (not all > closed terms of type nat are judgmentally equal to a numeral), but I don't > think that this is too much of a problem in practice as we can implement a > closed term evaluator inspired by the cubical set model for computing these > numerals (much like how Coq has vm/native_compute for efficient computation > of closed terms). Finally my little experiment indicates that having a comp > which doesn't compute doesn't affect the practical usability of this system > too much either. > > -- > Anders > > PS: Note that I didn't remove reversals in my small experiment as it would > require a bit more hacking and I didn't have time to do it, but there is no > fundamental problem in doing this and from my experience with cartesian > cubical type theory it is not too bad in practice either (we would drop > reversals and instead have comp 0->1 and comp 1->0). > > > On Monday, October 1, 2018 at 9:02:53 AM UTC-4, coquand wrote: >> >> Following the previous note on semantics of HIT in the simplicial set >> model, I looked >> a little more at the formal system which is similar to cubical type >> theory (based on distributive >> lattices) but where the filling operation is treated as a -constant- >> (without any computation rule). >> >> This formal system has models in simplicial and cubical sets. >> >> It is possible to show for this system a canonicity theorem, similar to >> Voevodsky’s conjecture: a closed >> term of type Bool is -path equal- to 0 or 1. (With a similar statement >> for natural numbers.) >> >> A corollary of this result is that the value of such a closed term is >> the same in all models. Hence >> we know that the computation of such a closed term in various extensions >> where we can compute >> the filling operation will give the same value (and the same value which >> we get in simplicial set; so e.g. >> Brunerie constant has to be +/-2 in the model based on de Morgan >> algebras). >> >> This is proved using the sconing technique as described in >> >> >> https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html >> >> As is stated there, the problem for using this technique to solve >> Voevodsky’s conjecture is that there >> s no apparent way to associate (in a “strict” way) a simplicial/cubical >> set to a closed type in dependent >> type theory with identity types. >> >> This issue disappears here thanks to the use of higher dimensional >> syntax. >> >> I wrote a proof <http://www.cse.chalmers.se/~coquand/can3.pdf>which is >> the result of several discussions with Simon Huber and Christian Sattler >> on this topic. The proof can be done effectively using the cubical set >> model, or non effectively using the simplicial >> set model. >> Maybe a similar result can be proved for simplicial/cubical tribes. >> >> Thierry >> >> >> On 14 Sep 2018, at 16:16, Andrew Swan <wakeli...@gmail.com> wrote: >> >> Thanks for writing out the note. I'll also make a few remarks about how >> my more recent work connects with these things. >> >> 1. The initial Susp X algebras, and I think in fact all of the initial >> algebras appearing in the Coquand-Huber-Mortberg paper, can be constructed >> by combining finite colimits and W types with reductions (as appearing in >> this paper <https://arxiv.org/abs/1802.07588>). From this it follows >> that they exist not just in cubical sets and simplicial sets, but any topos >> that satisfies WISC, and for the special case of presheaf categories with >> locally decidable cofibrations they can be constructed without using WISC >> or exact quotients. I think the latter can be viewed as a generalisation of >> the Coquand-Huber-Mortberg definition. >> >> 2. In my post and again in the W-types with reductions paper I suggested >> using Christian's generalised notion of lifting property for commutative >> squares. I still think this works, but I now lean towards other ways of >> looking at it. I didn't really emphasise this in the paper, but it follows >> from the general theory that one obtains not just an awfs, but a fibred >> awfs over the codomain fibration. This gives an awfs, and thereby a notion >> of trivial cofibration and fibration for each slice category C/Y. Then >> given a map f : X -> Y, we can either view it as a map in the slice >> category C/1 and factorise it there or as a map into the terminal object in >> the slice category C/Y. The latter is necessarily stable under pullback, >> and I think works out the same as "freely adding a homogeneous filling >> operator." >> >> Alternatively, it is also possible to use W types with reductions >> directly, without going via the small object argument. In this case the >> proofs in the Coquand-Huber-Mortberg paper generalise pretty much directly >> with very little modification. >> >> 3. I still find the situation in simplicial sets a little strange, in >> particular the need to switch back and forth between the different notions >> of fibration, although it does work as far as I can tell. >> >> 4. I made some remarks before about universal lifting problems. These now >> appear in the paper Lifting Problems in Grothendieck Fibrations >> <https://arxiv.org/abs/1802.06718> . >> >> Best, >> Andrew >> >> >> On Friday, 14 September 2018 13:15:58 UTC+2, coquand wrote: >>> >>> >>> I wrote a short note <http://www.cse.chalmers.se/~coquand/hits.pdf> to >>> confirm Andrew’s message that indeed this technique >>> works as well (using classical logic) for simplicial sets. This can now >>> be presented >>> as a combination of various published results. (The originality is only >>> in the presentation; >>> this essentially follows what is suggested in Andrew’s message.) >>> This provides a semantics of e.g. suspension as an operation U -> U, >>> where U >>> is an univalent universe in the simplicial set model. >>> >>> Thierry >>> >>> >>> On 7 Jun 2017, at 14:34, Andrew Swan <wakeli...@gmail.com> wrote: >>> >>> So suspension (or more generally pushouts/coequalisers) is what would >>>> make a really good test case for any proposed general approach — it’s the >>>> simplest HIT which as far as I know hasn’t been modelled without a size >>>> blowup in any infinite-dimensional model except cubical sets, under any of >>>> the approaches to modelling HIT’s proposed so far. (Am I right in >>>> remembering that this has been given for cubical sets? I can’t find it in >>>> any of the writeups, but I seem to recall hearing it presented at >>>> conferences.) >>> >>> >>> The technique used in cubical type theory seems fairly flexible. I'm not >>> sure exactly how flexible, but I think I can get suspension to work in >>> simplicial sets. In the below, throughout I use the characterisation of >>> fibrations as maps with the rlp against the pushout product of each >>> monomorphism with endpoint inclusion into the interval. WLOG there is also >>> a uniformity condition - we have a choice of lift and "pulling back the >>> monomorphism preserves the lift." >>> >>> Given a fibration X -> Y, you first freely add elements N and S together >>> with a path from N to S for each element of X (I think this is the same as >>> what you called pre suspension). Although the pre suspension is not a >>> fibration in general, it does have some of the properties you might expect >>> from a fibration. Given a path in Y, and an element in the fibre of an >>> endpoint, one can transport along the path to get something in the fibre of >>> the other endpoint. There should also be a "flattening" operation that >>> takes a path q in presuspension(X) over p in Y, and returns a path from >>> q(1) to the transport along p of q(0) that lies entirely in the fibre of >>> p(1). >>> >>> You then take the "weak fibrant replacement" of the pre suspension. A >>> map in simplicial sets is a fibration if and only if it has the rlp against >>> each pushout product of a monomorphism with an endpoint inclusion into the >>> interval. In fibrant replacement you freely add a diagonal lift for each >>> such lifting problems. In weak fibrant replacement you only add fillers for >>> some of these lifting problems. The pushout product of a monomorphism A -> >>> B with endpoint inclusion always has codomain B x I - then only consider >>> those lifting problems where the bottom map factors through the projection >>> B x I -> B. I think there are two ways to ensure that the operation of weak >>> fibrant replacement is stable under pullback - one way is carry out the >>> operation "internally" in simplicial sets (viewed as a topos), and the >>> other to use the algebraic small object argument, ensuring that uniformity >>> condition above is in the definition. The intuitive reason why this should >>> be stable is that the problem that stops the usual fibrant replacement from >>> being stable is that e.g. when we freely add the transport of a point along >>> a path, p we are adding a new element to the fibre of p(1) which depends on >>> things outside of that fibre, whereas with weak fibrant replacement we only >>> add a filler to an open box to a certain fibre if the original open box >>> lies entirely in that fibre. >>> >>> In order to show that the suspension is fibrant one has to use both the >>> structure already present in pre suspension (transport and flattening) and >>> the additional structure added by weak fibrant replacement. The idea is to >>> follow the same proof as for cubical type theory. It is enough to just show >>> composition and then derive filling. So to define the composition of an >>> open box, first flatten it, then use the weak fibration structure to find >>> the composition. (And I think that last part should be an instance of a >>> general result along the lines of "if the monad of transport and flattening >>> distributes over a monad, then the fibrant replacement monad distributes >>> over the coproduct of that monad with weak fibrant replacement"). >>> >>> >>> Best, >>> Andrew >>> >>> >>> On Wednesday, 7 June 2017 11:40:12 UTC+2, Peter LeFanu Lumsdaine wrote: >>>> >>>> On Thu, Jun 1, 2017 at 6:08 PM, Peter LeFanu Lumsdaine < >>>> p.l.lu...@gmail.com> 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. >>>>> >>>> >>>> I realise I was a bit unclear here: it’s only suspension that I meant >>>> to suggest is problematic, not propositional truncation. The latter seems >>>> a bit easier to do by ad hoc constructions; e.g. the construction below >>>> does it in simplicial sets, and I think a similar thing may work also in >>>> cubical sets. (I don’t claim originality for this construction; I don’t >>>> think I learned it from anywhere, but I do recall discussing it with people >>>> who were already aware of it or something similar (I think at least Mike, >>>> Thierry, and Simon Huber, at various times?), so I think multiple people >>>> may have noticed it independently.) >>>> >>>> So suspension (or more generally pushouts/coequalisers) is what would >>>> make a really good test case for any proposed general approach — it’s the >>>> simplest HIT which as far as I know hasn’t been modelled without a size >>>> blowup in any infinite-dimensional model except cubical sets, under any of >>>> the approaches to modelling HIT’s proposed so far. (Am I right in >>>> remembering that this has been given for cubical sets? I can’t find it in >>>> any of the writeups, but I seem to recall hearing it presented at >>>> conferences.) >>>> >>>> Construction of propositional truncation without size blowup in >>>> simplicial sets: >>>> >>>> (1) Given a fibration Y —> X, define |Y| —> X as follows: >>>> >>>> an element of |Y|_n consists of an n-simplex x : Δ[n] —> X, together >>>> with a “partial lift of x into Y, defined at least on all vertices”, i.e. a >>>> subpresheaf S ≤ Δ[n] containing all vertices, and a map y : S —> Y such >>>> that the evident square commutes; >>>> >>>> reindexing acts by taking pullbacks/inverse images of the domain of the >>>> partial lift (i.e. the usual composition of a partial map with a total map). >>>> >>>> (2) There’s an evident map Y —> |Y| over X; and the operation sending Y >>>> to Y —> |Y| —> X is (coherently) stable up to isomorphism under pullback in >>>> X. (Straightforward.) >>>> >>>> (3) In general, a fibration is a proposition in the type-theoretic >>>> sense iff it’s orthogonal to the boundary inclusions δ[n] —> Δ[n] for all n >>>> > 0. (Non-trivial but not too hard to check.) >>>> >>>> (4) The map |Y| —> X is a fibration, and a proposition. >>>> (Straightforward, given (3), by concretely constructing the required >>>> liftings.) >>>> >>>> (5) The evident map Y —> |Y| over X is a cell complex constructed from >>>> boundary inclusions δ[n] —> Δ[n] with n > 0. >>>> >>>> To see this: take the filtration of |Y| by subobjects Y_n, where the >>>> non-degenerate simplices of Y_n are those whose “missing” simplices are all >>>> of dimension ≤n. Then Y_0 = Y, and the non-degenerate simplices of Y_{n+1} >>>> that are not in Y_n are all {n+1}-cells with boundary in Y_n, so the >>>> inclusion Y_n —> Y_{n+1} may be seen as gluing on many copies of δ[n+1] —> >>>> Δ[n+1]. >>>> >>>> (6) The map Y —> |Y| is orthogonal to all propositional fibrations, >>>> stably in X. (Orthogonality is immediate from (3) and (5); stability is >>>> then by (2).) >>>> >>>> (7) Let V be either the universe of “well-ordered α-small fibrations”, >>>> or the universe of “displayed α-small fibrations”, for α any infinite >>>> regular cardinal. Then V carries an operation representing the >>>> construction of (1), and modelling propositional truncation. (Lengthy to >>>> spell out in full, but straightforward given (2), (6).) >>>> >>>> >>>> –p. >>>> >>>> >>>> >>>> >>> >> -- >> 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+unsubscribe@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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 24824 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-01 15:30 ` Steve Awodey 2017-06-01 15:38 ` Michael Shulman @ 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA 2018-11-12 12:30 ` Ali Caglayan 1 sibling, 1 reply; 25+ messages in thread From: CARLOS MANUEL MANZUETA @ 2017-06-08 4:57 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 32 bytes --] Where I could find the L-S paper ^ permalink raw reply [flat|nested] 25+ messages in thread
* Re: [HoTT] Semantics of higher inductive types 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA @ 2018-11-12 12:30 ` Ali Caglayan 0 siblings, 0 replies; 25+ messages in thread From: Ali Caglayan @ 2018-11-12 12:30 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 443 bytes --] https://arxiv.org/abs/1705.07088 On Thursday, 8 June 2017 05:57:17 UTC+1, CARLOS MANUEL MANZUETA wrote: > > Where I could find the L-S paper -- 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+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 764 bytes --] ^ permalink raw reply [flat|nested] 25+ messages in thread
end of thread, other threads:[~2018-11-12 12:30 UTC | newest] Thread overview: 25+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-05-25 18:25 Semantics of higher inductive types Michael Shulman 2017-05-26 0:17 ` [HoTT] " Emily Riehl 2017-06-01 14:23 ` Thierry Coquand 2017-06-01 14:43 ` Michael Shulman 2017-06-01 15:30 ` Steve Awodey 2017-06-01 15:38 ` Michael Shulman 2017-06-01 15:56 ` Steve Awodey 2017-06-01 16:08 ` Peter LeFanu Lumsdaine 2017-06-06 9:19 ` Andrew Swan 2017-06-06 10:03 ` Andrew Swan 2017-06-06 13:35 ` Michael Shulman 2017-06-06 16:22 ` Andrew Swan 2017-06-06 19:36 ` Michael Shulman 2017-06-06 20:59 ` Andrew Swan 2017-06-07 9:40 ` Peter LeFanu Lumsdaine 2017-06-07 9:57 ` Thierry Coquand [not found] ` <ed7ad345-85e4-4536-86d7-a57fbe3313fe@googlegroups.com> 2017-06-07 23:06 ` Michael Shulman 2017-06-08 6:35 ` Andrew Swan 2018-09-14 11:15 ` Thierry Coquand 2018-09-14 14:16 ` Andrew Swan 2018-10-01 13:02 ` Thierry Coquand 2018-11-10 15:52 ` Anders Mörtberg 2018-11-10 18:21 ` Gabriel Scherer 2017-06-08 4:57 ` CARLOS MANUEL MANZUETA 2018-11-12 12:30 ` Ali Caglayan
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).