* Quillen model structure @ 2018-06-10 13:31 Thierry Coquand [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com> ` (2 more replies) 0 siblings, 3 replies; 21+ messages in thread From: Thierry Coquand @ 2018-06-10 13:31 UTC (permalink / raw) To: Homotopy Theory [-- Attachment #1.1: Type: text/plain, Size: 2768 bytes --] The attached note contains two connected results: (1) a concrete description of the trivial cofibration-fibration factorisation for cartesian cubical sets It follows from this using results of section 2 of Christian Sattler’s paper https://arxiv.org/pdf/1704.06911 that we have a model structure on cartesian cubical sets (that we can call “type-theoretic” since it is built on ideas coming from type theory), which can be done in a constructive setting. The fibrant objects of this model structure form a model of type theory with universes (and conversely the fact that we have a fibrant universe is a crucial component in the proof that we have a model structure). I described essentially the same argument for factorisation in a message to this list last year July 6, 2017 (for another notion of cubical sets however): no quotient operation is involved in contrast with the "small object argument”. This kind of factorisation has been described in a more general framework in the paper of Andrew Swan https://arxiv.org/abs/1802.07588 Since there is a canonical geometric realisation of cartesian cubical sets (realising the formal interval as the real unit interval [0,1]) a natural question is if this is a Quillen equivalence. The second result, due to Christian Sattler, is that (2) the geometric realisation map is -not- a Quillen equivalence. I believe that this result should be relevant even for people interested in the more syntactic aspects of type theory. It implies that if we extend cartesian cubical type theory with a type which is a HIT built from a primitive symmetric square q(x,y) = q(y,z), we get a type which should be contractible (at least its geometric realisation is) but we cannot show this in cartesian cubical type theory. It is thus important to understand better what is going on, and this is why I post this note, The point (2) is only a concrete description of Sattler’s argument he presented last week at the HIM meeting. Ulrik Buchholtz has (independently) more abstract proofs of similar results (not for cartesian cubical sets however), which should bring further lights on this question. Note that this implies that the canonical map Cartesian cubes -> Dedekind cubes (corresponding to distributive lattices) is also not a Quillen equivalence (for their respective type theoretic model structures). Hence, as noted by Steve, this implies that the model structure obtained by transfer and described at https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf is not equivalent to the type-theoretic model structure. Thierry PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions about this last week in Bonn. [-- Attachment #1.2: Type: text/html, Size: 4870 bytes --] [-- Attachment #2: fact1.pdf --] [-- Type: application/pdf, Size: 168794 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
[parent not found: <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com>]
* Re: [HoTT] Quillen model structure [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com> @ 2018-06-11 8:46 ` Thierry Coquand 0 siblings, 0 replies; 21+ messages in thread From: Thierry Coquand @ 2018-06-11 8:46 UTC (permalink / raw) To: Hiroyuki Miyoshi; +Cc: Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 3936 bytes --] Hello Sorry for this problem. I should have used the following link https://ncatlab.org/homotopytypetheory/files/awodeyMURI18.pdf Best regards, Thierry On 11 Jun 2018, at 10:28, Hiroyuki Miyoshi <h...@cc.kyoto-su.ac.jp<mailto:h...@cc.kyoto-su.ac.jp>> wrote: Hi, Thierry, Your note is very interesting for me! Unfortunately, the Awodey's filie you mentioned in your message seems to be (still?) private and I cannot read it: https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf If you (or Steve?) can change the status of the file, please make it public. Thanks in advance. Hiroyuki Miyoshi, Dept of Mathematics, Kyoto Sangyo University, Kyoto, Japan h...@cc.kyoto-su.ac.jp<mailto:h...@cc.kyoto-su.ac.jp> 2018年6月10日(日) 22:31 Thierry Coquand <Thierry...@cse.gu.se<mailto:Thierry...@cse.gu.se>>: The attached note contains two connected results: (1) a concrete description of the trivial cofibration-fibration factorisation for cartesian cubical sets It follows from this using results of section 2 of Christian Sattler’s paper https://arxiv.org/pdf/1704.06911 that we have a model structure on cartesian cubical sets (that we can call “type-theoretic” since it is built on ideas coming from type theory), which can be done in a constructive setting. The fibrant objects of this model structure form a model of type theory with universes (and conversely the fact that we have a fibrant universe is a crucial component in the proof that we have a model structure). I described essentially the same argument for factorisation in a message to this list last year July 6, 2017 (for another notion of cubical sets however): no quotient operation is involved in contrast with the "small object argument”. This kind of factorisation has been described in a more general framework in the paper of Andrew Swan https://arxiv.org/abs/1802.07588 Since there is a canonical geometric realisation of cartesian cubical sets (realising the formal interval as the real unit interval [0,1]) a natural question is if this is a Quillen equivalence. The second result, due to Christian Sattler, is that (2) the geometric realisation map is -not- a Quillen equivalence. I believe that this result should be relevant even for people interested in the more syntactic aspects of type theory. It implies that if we extend cartesian cubical type theory with a type which is a HIT built from a primitive symmetric square q(x,y) = q(y,z), we get a type which should be contractible (at least its geometric realisation is) but we cannot show this in cartesian cubical type theory. It is thus important to understand better what is going on, and this is why I post this note, The point (2) is only a concrete description of Sattler’s argument he presented last week at the HIM meeting. Ulrik Buchholtz has (independently) more abstract proofs of similar results (not for cartesian cubical sets however), which should bring further lights on this question. Note that this implies that the canonical map Cartesian cubes -> Dedekind cubes (corresponding to distributive lattices) is also not a Quillen equivalence (for their respective type theoretic model structures). Hence, as noted by Steve, this implies that the model structure obtained by transfer and described at https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf is not equivalent to the type-theoretic model structure. Thierry PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions about this last week in Bonn. -- 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. [-- Attachment #2: Type: text/html, Size: 16205 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-10 13:31 Quillen model structure Thierry Coquand [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com> @ 2018-06-13 20:33 ` Michael Shulman 2018-06-13 20:50 ` Steve Awodey 2018-06-14 18:39 ` Richard Williamson 2 siblings, 1 reply; 21+ messages in thread From: Michael Shulman @ 2018-06-13 20:33 UTC (permalink / raw) To: Thierry Coquand; +Cc: Homotopy Theory This is very interesting. Does it mean that the (oo,1)-category presented by this model category of cartesian cubical sets is a (complete and cocomplete) elementary (oo,1)-topos that is not a Grothendieck (oo,1)-topos? On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand <Thierry...@cse.gu.se> wrote: > The attached note contains two connected results: > > (1) a concrete description of the trivial cofibration-fibration > factorisation for cartesian > cubical sets > > It follows from this using results of section 2 of Christian Sattler’s > paper > > https://arxiv.org/pdf/1704.06911 > > that we have a model structure on cartesian cubical sets (that we can call > “type-theoretic” > since it is built on ideas coming from type theory), which can be done in a > constructive > setting. The fibrant objects of this model structure form a model of type > theory with universes > (and conversely the fact that we have a fibrant universe is a crucial > component in the proof > that we have a model structure). > > I described essentially the same argument for factorisation in a message > to this list last year > July 6, 2017 (for another notion of cubical sets however): no quotient > operation is involved > in contrast with the "small object argument”. > This kind of factorisation has been described in a more general framework > in the paper of Andrew Swan > > https://arxiv.org/abs/1802.07588 > > > > Since there is a canonical geometric realisation of cartesian cubical sets > (realising the formal > interval as the real unit interval [0,1]) a natural question is if this is a > Quillen equivalence. > The second result, due to Christian Sattler, is that > > (2) the geometric realisation map is -not- a Quillen equivalence. > > I believe that this result should be relevant even for people interested in > the more syntactic > aspects of type theory. It implies that if we extend cartesian cubical type > theory > with a type which is a HIT built from a primitive symmetric square q(x,y) = > q(y,z), we get a type > which should be contractible (at least its geometric realisation is) but we > cannot show this in > cartesian cubical type theory. > > It is thus important to understand better what is going on, and this is why > I post this note, > The point (2) is only a concrete description of Sattler’s argument he > presented last week at the HIM > meeting. Ulrik Buchholtz has (independently) > more abstract proofs of similar results (not for cartesian cubical sets > however), which should bring > further lights on this question. > > Note that this implies that the canonical map Cartesian cubes -> Dedekind > cubes (corresponding > to distributive lattices) is also not a Quillen equivalence (for their > respective type theoretic model > structures). Hence, as noted by Steve, this implies that the model structure > obtained by transfer > and described at > > https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf > > is not equivalent to the type-theoretic model structure. > > Thierry > > PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions > about this last week in Bonn. > > -- > 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-13 20:33 ` Michael Shulman @ 2018-06-13 20:50 ` Steve Awodey 2018-06-13 22:00 ` Michael Shulman 0 siblings, 1 reply; 21+ messages in thread From: Steve Awodey @ 2018-06-13 20:50 UTC (permalink / raw) To: Michael Shulman; +Cc: Thierry Coquand, Homotopy Theory oh, interesting! because it’s not defined over sSet, but is covered by it. > On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote: > > This is very interesting. Does it mean that the (oo,1)-category > presented by this model category of cartesian cubical sets is a > (complete and cocomplete) elementary (oo,1)-topos that is not a > Grothendieck (oo,1)-topos? > > On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand > <Thierry...@cse.gu.se> wrote: >> The attached note contains two connected results: >> >> (1) a concrete description of the trivial cofibration-fibration >> factorisation for cartesian >> cubical sets >> >> It follows from this using results of section 2 of Christian Sattler’s >> paper >> >> https://arxiv.org/pdf/1704.06911 >> >> that we have a model structure on cartesian cubical sets (that we can call >> “type-theoretic” >> since it is built on ideas coming from type theory), which can be done in a >> constructive >> setting. The fibrant objects of this model structure form a model of type >> theory with universes >> (and conversely the fact that we have a fibrant universe is a crucial >> component in the proof >> that we have a model structure). >> >> I described essentially the same argument for factorisation in a message >> to this list last year >> July 6, 2017 (for another notion of cubical sets however): no quotient >> operation is involved >> in contrast with the "small object argument”. >> This kind of factorisation has been described in a more general framework >> in the paper of Andrew Swan >> >> https://arxiv.org/abs/1802.07588 >> >> >> >> Since there is a canonical geometric realisation of cartesian cubical sets >> (realising the formal >> interval as the real unit interval [0,1]) a natural question is if this is a >> Quillen equivalence. >> The second result, due to Christian Sattler, is that >> >> (2) the geometric realisation map is -not- a Quillen equivalence. >> >> I believe that this result should be relevant even for people interested in >> the more syntactic >> aspects of type theory. It implies that if we extend cartesian cubical type >> theory >> with a type which is a HIT built from a primitive symmetric square q(x,y) = >> q(y,z), we get a type >> which should be contractible (at least its geometric realisation is) but we >> cannot show this in >> cartesian cubical type theory. >> >> It is thus important to understand better what is going on, and this is why >> I post this note, >> The point (2) is only a concrete description of Sattler’s argument he >> presented last week at the HIM >> meeting. Ulrik Buchholtz has (independently) >> more abstract proofs of similar results (not for cartesian cubical sets >> however), which should bring >> further lights on this question. >> >> Note that this implies that the canonical map Cartesian cubes -> Dedekind >> cubes (corresponding >> to distributive lattices) is also not a Quillen equivalence (for their >> respective type theoretic model >> structures). Hence, as noted by Steve, this implies that the model structure >> obtained by transfer >> and described at >> >> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >> >> is not equivalent to the type-theoretic model structure. >> >> Thierry >> >> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >> about this last week in Bonn. >> >> -- >> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-13 20:50 ` Steve Awodey @ 2018-06-13 22:00 ` Michael Shulman 2018-06-14 9:28 ` Steve Awodey 0 siblings, 1 reply; 21+ messages in thread From: Michael Shulman @ 2018-06-13 22:00 UTC (permalink / raw) To: Steve Awodey; +Cc: Thierry Coquand, Homotopy Theory In the 1-categorical case, I believe that every locally small (co)complete elementary 1-topos is defined over Set: its global sections functor has a left adjoint by cocompleteness, and the left adjoint is left exact by the Giraud exactness properties (which hold for any (co)complete elementary 1-topos). Such a topos can only fail to be Grothendieck by lacking a small generating set. In the oo-case, certainly cartesian cubical sets present a locally small (oo,1)-category (any model category does, at least assuming its locally small as a 1-category), so it seems to me there are three possibilities: 1. Although they are presumably an "elementary (oo,1)-topos" in the finitary sense that provides semantics for HoTT with HITs and univalent universes, they might fail to satisfy some of the oo-Giraud exactness properties. Presumably they are locally cartesian closed and coproducts are disjoint, so it would have to be that not all groupoids are effective. 2. They might lack a small generating set, i.e. the (oo,1)-category might not be locally presentable. Every combinatorial model category (i.e. cofibrantly generated model structure on a locally presentable 1-category) presents a locally presentable (oo,1)-category, and the 1-category of cartesian cubical sets is certainly locally presentable, but I suppose it's not obvious whether these weak factorization systems are cofibrantly generated. 3. They might be a Grothendieck (oo,1)-topos after all. I don't know which of these is most likely; they all seem strange. On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: > oh, interesting! > because it’s not defined over sSet, but is covered by it. > >> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote: >> >> This is very interesting. Does it mean that the (oo,1)-category >> presented by this model category of cartesian cubical sets is a >> (complete and cocomplete) elementary (oo,1)-topos that is not a >> Grothendieck (oo,1)-topos? >> >> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >> <Thierry...@cse.gu.se> wrote: >>> The attached note contains two connected results: >>> >>> (1) a concrete description of the trivial cofibration-fibration >>> factorisation for cartesian >>> cubical sets >>> >>> It follows from this using results of section 2 of Christian Sattler’s >>> paper >>> >>> https://arxiv.org/pdf/1704.06911 >>> >>> that we have a model structure on cartesian cubical sets (that we can call >>> “type-theoretic” >>> since it is built on ideas coming from type theory), which can be done in a >>> constructive >>> setting. The fibrant objects of this model structure form a model of type >>> theory with universes >>> (and conversely the fact that we have a fibrant universe is a crucial >>> component in the proof >>> that we have a model structure). >>> >>> I described essentially the same argument for factorisation in a message >>> to this list last year >>> July 6, 2017 (for another notion of cubical sets however): no quotient >>> operation is involved >>> in contrast with the "small object argument”. >>> This kind of factorisation has been described in a more general framework >>> in the paper of Andrew Swan >>> >>> https://arxiv.org/abs/1802.07588 >>> >>> >>> >>> Since there is a canonical geometric realisation of cartesian cubical sets >>> (realising the formal >>> interval as the real unit interval [0,1]) a natural question is if this is a >>> Quillen equivalence. >>> The second result, due to Christian Sattler, is that >>> >>> (2) the geometric realisation map is -not- a Quillen equivalence. >>> >>> I believe that this result should be relevant even for people interested in >>> the more syntactic >>> aspects of type theory. It implies that if we extend cartesian cubical type >>> theory >>> with a type which is a HIT built from a primitive symmetric square q(x,y) = >>> q(y,z), we get a type >>> which should be contractible (at least its geometric realisation is) but we >>> cannot show this in >>> cartesian cubical type theory. >>> >>> It is thus important to understand better what is going on, and this is why >>> I post this note, >>> The point (2) is only a concrete description of Sattler’s argument he >>> presented last week at the HIM >>> meeting. Ulrik Buchholtz has (independently) >>> more abstract proofs of similar results (not for cartesian cubical sets >>> however), which should bring >>> further lights on this question. >>> >>> Note that this implies that the canonical map Cartesian cubes -> Dedekind >>> cubes (corresponding >>> to distributive lattices) is also not a Quillen equivalence (for their >>> respective type theoretic model >>> structures). Hence, as noted by Steve, this implies that the model structure >>> obtained by transfer >>> and described at >>> >>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>> >>> is not equivalent to the type-theoretic model structure. >>> >>> Thierry >>> >>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >>> about this last week in Bonn. >>> >>> -- >>> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-13 22:00 ` Michael Shulman @ 2018-06-14 9:28 ` Steve Awodey 2018-06-14 9:48 ` Bas Spitters 2018-06-14 9:58 ` Christian Sattler 0 siblings, 2 replies; 21+ messages in thread From: Steve Awodey @ 2018-06-14 9:28 UTC (permalink / raw) To: Michael Shulman; +Cc: Thierry Coquand, Homotopy Theory > On Jun 14, 2018, at 12:00 AM, Michael Shulman <shu...@sandiego.edu> wrote: > > In the 1-categorical case, I believe that every locally small > (co)complete elementary 1-topos is defined over Set: its global > sections functor has a left adjoint by cocompleteness, and the left > adjoint is left exact by the Giraud exactness properties (which hold > for any (co)complete elementary 1-topos). Such a topos can only fail > to be Grothendieck by lacking a small generating set. yes, that’s correct. > > In the oo-case, certainly cartesian cubical sets present a locally > small (oo,1)-category (any model category does, at least assuming its > locally small as a 1-category), so it seems to me there are three > possibilities: > > 1. Although they are presumably an "elementary (oo,1)-topos" in the > finitary sense that provides semantics for HoTT with HITs and > univalent universes, they might fail to satisfy some of the oo-Giraud > exactness properties. Presumably they are locally cartesian closed > and coproducts are disjoint, so it would have to be that not all > groupoids are effective. that’s possible, I suppose … > > 2. They might lack a small generating set, i.e. the (oo,1)-category > might not be locally presentable. Every combinatorial model category > (i.e. cofibrantly generated model structure on a locally presentable > 1-category) presents a locally presentable (oo,1)-category, and the > 1-category of cartesian cubical sets is certainly locally presentable, > but I suppose it's not obvious whether these weak factorization > systems are cofibrantly generated. but they are cofibrantly generated: - the cofibrations can be taken to be all monos (say), which are generated by subobjects of cubes as usual, and - the trivial cofibrations are generated by certain subobjects U >—> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, a small set of generating trivial cofibrations. Steve > > 3. They might be a Grothendieck (oo,1)-topos after all. > > I don't know which of these is most likely; they all seem strange. > > > > > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: >> oh, interesting! >> because it’s not defined over sSet, but is covered by it. >> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote: >>> >>> This is very interesting. Does it mean that the (oo,1)-category >>> presented by this model category of cartesian cubical sets is a >>> (complete and cocomplete) elementary (oo,1)-topos that is not a >>> Grothendieck (oo,1)-topos? >>> >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >>> <Thierry...@cse.gu.se> wrote: >>>> The attached note contains two connected results: >>>> >>>> (1) a concrete description of the trivial cofibration-fibration >>>> factorisation for cartesian >>>> cubical sets >>>> >>>> It follows from this using results of section 2 of Christian Sattler’s >>>> paper >>>> >>>> https://arxiv.org/pdf/1704.06911 >>>> >>>> that we have a model structure on cartesian cubical sets (that we can call >>>> “type-theoretic” >>>> since it is built on ideas coming from type theory), which can be done in a >>>> constructive >>>> setting. The fibrant objects of this model structure form a model of type >>>> theory with universes >>>> (and conversely the fact that we have a fibrant universe is a crucial >>>> component in the proof >>>> that we have a model structure). >>>> >>>> I described essentially the same argument for factorisation in a message >>>> to this list last year >>>> July 6, 2017 (for another notion of cubical sets however): no quotient >>>> operation is involved >>>> in contrast with the "small object argument”. >>>> This kind of factorisation has been described in a more general framework >>>> in the paper of Andrew Swan >>>> >>>> https://arxiv.org/abs/1802.07588 >>>> >>>> >>>> >>>> Since there is a canonical geometric realisation of cartesian cubical sets >>>> (realising the formal >>>> interval as the real unit interval [0,1]) a natural question is if this is a >>>> Quillen equivalence. >>>> The second result, due to Christian Sattler, is that >>>> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>>> >>>> I believe that this result should be relevant even for people interested in >>>> the more syntactic >>>> aspects of type theory. It implies that if we extend cartesian cubical type >>>> theory >>>> with a type which is a HIT built from a primitive symmetric square q(x,y) = >>>> q(y,z), we get a type >>>> which should be contractible (at least its geometric realisation is) but we >>>> cannot show this in >>>> cartesian cubical type theory. >>>> >>>> It is thus important to understand better what is going on, and this is why >>>> I post this note, >>>> The point (2) is only a concrete description of Sattler’s argument he >>>> presented last week at the HIM >>>> meeting. Ulrik Buchholtz has (independently) >>>> more abstract proofs of similar results (not for cartesian cubical sets >>>> however), which should bring >>>> further lights on this question. >>>> >>>> Note that this implies that the canonical map Cartesian cubes -> Dedekind >>>> cubes (corresponding >>>> to distributive lattices) is also not a Quillen equivalence (for their >>>> respective type theoretic model >>>> structures). Hence, as noted by Steve, this implies that the model structure >>>> obtained by transfer >>>> and described at >>>> >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>>> >>>> is not equivalent to the type-theoretic model structure. >>>> >>>> Thierry >>>> >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >>>> about this last week in Bonn. >>>> >>>> -- >>>> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 9:28 ` Steve Awodey @ 2018-06-14 9:48 ` Bas Spitters 2018-06-14 9:58 ` Christian Sattler 1 sibling, 0 replies; 21+ messages in thread From: Bas Spitters @ 2018-06-14 9:48 UTC (permalink / raw) To: Steve Awodey, nicolas tabareau Cc: Michael Shulman, Thierry Coquand, Homotopy Theory There has been some work by Nicolas Tabareau's group to try and prove the exactness properties. E.g. https://homotopytypetheory.org/2016/01/08/colimits-in-hott/ https://jfr.unibo.it/article/download/6232/6389 and perhaps even later work. It would be interesting if the Cartesian cubes would provide a counterexample to this approach, and show that a 2-level type theory is really needed. On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote: > > >> On Jun 14, 2018, at 12:00 AM, Michael Shulman <shu...@sandiego.edu> wrote: >> >> In the 1-categorical case, I believe that every locally small >> (co)complete elementary 1-topos is defined over Set: its global >> sections functor has a left adjoint by cocompleteness, and the left >> adjoint is left exact by the Giraud exactness properties (which hold >> for any (co)complete elementary 1-topos). Such a topos can only fail >> to be Grothendieck by lacking a small generating set. > > yes, that’s correct. > >> >> In the oo-case, certainly cartesian cubical sets present a locally >> small (oo,1)-category (any model category does, at least assuming its >> locally small as a 1-category), so it seems to me there are three >> possibilities: >> >> 1. Although they are presumably an "elementary (oo,1)-topos" in the >> finitary sense that provides semantics for HoTT with HITs and >> univalent universes, they might fail to satisfy some of the oo-Giraud >> exactness properties. Presumably they are locally cartesian closed >> and coproducts are disjoint, so it would have to be that not all >> groupoids are effective. > > that’s possible, I suppose … > >> >> 2. They might lack a small generating set, i.e. the (oo,1)-category >> might not be locally presentable. Every combinatorial model category >> (i.e. cofibrantly generated model structure on a locally presentable >> 1-category) presents a locally presentable (oo,1)-category, and the >> 1-category of cartesian cubical sets is certainly locally presentable, >> but I suppose it's not obvious whether these weak factorization >> systems are cofibrantly generated. > > but they are cofibrantly generated: > > - the cofibrations can be taken to be all monos (say), which are generated by subobjects of cubes as usual, and > > - the trivial cofibrations are generated by certain subobjects U >—> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, a small set of generating trivial cofibrations. > > > Steve > >> >> 3. They might be a Grothendieck (oo,1)-topos after all. >> >> I don't know which of these is most likely; they all seem strange. >> > >> >> >> >> On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: >>> oh, interesting! >>> because it’s not defined over sSet, but is covered by it. >>> >>>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> wrote: >>>> >>>> This is very interesting. Does it mean that the (oo,1)-category >>>> presented by this model category of cartesian cubical sets is a >>>> (complete and cocomplete) elementary (oo,1)-topos that is not a >>>> Grothendieck (oo,1)-topos? >>>> >>>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >>>> <Thierry...@cse.gu.se> wrote: >>>>> The attached note contains two connected results: >>>>> >>>>> (1) a concrete description of the trivial cofibration-fibration >>>>> factorisation for cartesian >>>>> cubical sets >>>>> >>>>> It follows from this using results of section 2 of Christian Sattler’s >>>>> paper >>>>> >>>>> https://arxiv.org/pdf/1704.06911 >>>>> >>>>> that we have a model structure on cartesian cubical sets (that we can call >>>>> “type-theoretic” >>>>> since it is built on ideas coming from type theory), which can be done in a >>>>> constructive >>>>> setting. The fibrant objects of this model structure form a model of type >>>>> theory with universes >>>>> (and conversely the fact that we have a fibrant universe is a crucial >>>>> component in the proof >>>>> that we have a model structure). >>>>> >>>>> I described essentially the same argument for factorisation in a message >>>>> to this list last year >>>>> July 6, 2017 (for another notion of cubical sets however): no quotient >>>>> operation is involved >>>>> in contrast with the "small object argument”. >>>>> This kind of factorisation has been described in a more general framework >>>>> in the paper of Andrew Swan >>>>> >>>>> https://arxiv.org/abs/1802.07588 >>>>> >>>>> >>>>> >>>>> Since there is a canonical geometric realisation of cartesian cubical sets >>>>> (realising the formal >>>>> interval as the real unit interval [0,1]) a natural question is if this is a >>>>> Quillen equivalence. >>>>> The second result, due to Christian Sattler, is that >>>>> >>>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>>>> >>>>> I believe that this result should be relevant even for people interested in >>>>> the more syntactic >>>>> aspects of type theory. It implies that if we extend cartesian cubical type >>>>> theory >>>>> with a type which is a HIT built from a primitive symmetric square q(x,y) = >>>>> q(y,z), we get a type >>>>> which should be contractible (at least its geometric realisation is) but we >>>>> cannot show this in >>>>> cartesian cubical type theory. >>>>> >>>>> It is thus important to understand better what is going on, and this is why >>>>> I post this note, >>>>> The point (2) is only a concrete description of Sattler’s argument he >>>>> presented last week at the HIM >>>>> meeting. Ulrik Buchholtz has (independently) >>>>> more abstract proofs of similar results (not for cartesian cubical sets >>>>> however), which should bring >>>>> further lights on this question. >>>>> >>>>> Note that this implies that the canonical map Cartesian cubes -> Dedekind >>>>> cubes (corresponding >>>>> to distributive lattices) is also not a Quillen equivalence (for their >>>>> respective type theoretic model >>>>> structures). Hence, as noted by Steve, this implies that the model structure >>>>> obtained by transfer >>>>> and described at >>>>> >>>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>>>> >>>>> is not equivalent to the type-theoretic model structure. >>>>> >>>>> Thierry >>>>> >>>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >>>>> about this last week in Bonn. >>>>> >>>>> -- >>>>> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 9:28 ` Steve Awodey 2018-06-14 9:48 ` Bas Spitters @ 2018-06-14 9:58 ` Christian Sattler 2018-06-14 10:27 ` Steve Awodey 1 sibling, 1 reply; 21+ messages in thread From: Christian Sattler @ 2018-06-14 9:58 UTC (permalink / raw) To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 6203 bytes --] On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote: > but they are cofibrantly generated: > > - the cofibrations can be taken to be all monos (say), which are generated > by subobjects of cubes as usual, and > > - the trivial cofibrations are generated by certain subobjects U >—> > I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for > all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, > a small set of generating trivial cofibrations. > Those would be the objects of a category of algebraic generators. For generators of the underlying weak factorization systems, one would take any cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, and for trivial cofibrations the corresponding generators Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. > Steve > > > > > 3. They might be a Grothendieck (oo,1)-topos after all. > > > > I don't know which of these is most likely; they all seem strange. > > > > > > > > > > > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: > >> oh, interesting! > >> because it’s not defined over sSet, but is covered by it. > >> > >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> > wrote: > >>> > >>> This is very interesting. Does it mean that the (oo,1)-category > >>> presented by this model category of cartesian cubical sets is a > >>> (complete and cocomplete) elementary (oo,1)-topos that is not a > >>> Grothendieck (oo,1)-topos? > >>> > >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand > >>> <Thierry...@cse.gu.se> wrote: > >>>> The attached note contains two connected results: > >>>> > >>>> (1) a concrete description of the trivial cofibration-fibration > >>>> factorisation for cartesian > >>>> cubical sets > >>>> > >>>> It follows from this using results of section 2 of Christian Sattler’s > >>>> paper > >>>> > >>>> https://arxiv.org/pdf/1704.06911 > >>>> > >>>> that we have a model structure on cartesian cubical sets (that we can > call > >>>> “type-theoretic” > >>>> since it is built on ideas coming from type theory), which can be > done in a > >>>> constructive > >>>> setting. The fibrant objects of this model structure form a model of > type > >>>> theory with universes > >>>> (and conversely the fact that we have a fibrant universe is a crucial > >>>> component in the proof > >>>> that we have a model structure). > >>>> > >>>> I described essentially the same argument for factorisation in a > message > >>>> to this list last year > >>>> July 6, 2017 (for another notion of cubical sets however): no quotient > >>>> operation is involved > >>>> in contrast with the "small object argument”. > >>>> This kind of factorisation has been described in a more general > framework > >>>> in the paper of Andrew Swan > >>>> > >>>> https://arxiv.org/abs/1802.07588 > >>>> > >>>> > >>>> > >>>> Since there is a canonical geometric realisation of cartesian cubical > sets > >>>> (realising the formal > >>>> interval as the real unit interval [0,1]) a natural question is if > this is a > >>>> Quillen equivalence. > >>>> The second result, due to Christian Sattler, is that > >>>> > >>>> (2) the geometric realisation map is -not- a Quillen equivalence. > >>>> > >>>> I believe that this result should be relevant even for people > interested in > >>>> the more syntactic > >>>> aspects of type theory. It implies that if we extend cartesian > cubical type > >>>> theory > >>>> with a type which is a HIT built from a primitive symmetric square > q(x,y) = > >>>> q(y,z), we get a type > >>>> which should be contractible (at least its geometric realisation is) > but we > >>>> cannot show this in > >>>> cartesian cubical type theory. > >>>> > >>>> It is thus important to understand better what is going on, and this > is why > >>>> I post this note, > >>>> The point (2) is only a concrete description of Sattler’s argument he > >>>> presented last week at the HIM > >>>> meeting. Ulrik Buchholtz has (independently) > >>>> more abstract proofs of similar results (not for cartesian cubical > sets > >>>> however), which should bring > >>>> further lights on this question. > >>>> > >>>> Note that this implies that the canonical map Cartesian cubes -> > Dedekind > >>>> cubes (corresponding > >>>> to distributive lattices) is also not a Quillen equivalence (for their > >>>> respective type theoretic model > >>>> structures). Hence, as noted by Steve, this implies that the model > structure > >>>> obtained by transfer > >>>> and described at > >>>> > >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf > >>>> > >>>> is not equivalent to the type-theoretic model structure. > >>>> > >>>> Thierry > >>>> > >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for > discussions > >>>> about this last week in Bonn. > >>>> > >>>> -- > >>>> 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: 10550 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 9:58 ` Christian Sattler @ 2018-06-14 10:27 ` Steve Awodey 2018-06-14 13:44 ` Steve Awodey 0 siblings, 1 reply; 21+ messages in thread From: Steve Awodey @ 2018-06-14 10:27 UTC (permalink / raw) To: Christian Sattler; +Cc: Michael Shulman, Thierry Coquand, Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 8272 bytes --] > On Jun 14, 2018, at 11:58 AM, Christian Sattler <sattler....@gmail.com> wrote: > > On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: > but they are cofibrantly generated: > > - the cofibrations can be taken to be all monos (say), which are generated by subobjects of cubes as usual, and > > - the trivial cofibrations are generated by certain subobjects U >—> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, a small set of generating trivial cofibrations. > > Those would be the objects of a category of algebraic generators. For generators of the underlying weak factorization systems, one would take any cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, this determines the same class of cofibrations as simply taking *all* subobjects of representables, which is already a set. There is no reason to act by Aut(n), etc., here. > and for trivial cofibrations the corresponding generators Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. sorry, I can’t read your notation. the generating trivial cofibrations I stated are the following: take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we can also regard as a mono over I by composition with j. Over I we also have the generic point d : I —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I . Then we forget the indexing over I to end up with the description I already gave, namely: U = I^n +_A (A x I) where the indexing j is built into the pushout over A. A more direct description is this: let h : I^n —> I^n x I be the graph of j, let g : A —> A x I be the graph of j.m, there is a commutative square: g A —— > A x I | | m | | m x I | | v v I^n ——> I^n x I | h j | v I put the usual pushout U = I^n +_A (A x I) inside it, and the comprison map U —> I^n x I is the m xo d mentioned above. Steve > > > Steve > > > > > 3. They might be a Grothendieck (oo,1)-topos after all. > > > > I don't know which of these is most likely; they all seem strange. > > > > > > > > > > > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: > >> oh, interesting! > >> because it’s not defined over sSet, but is covered by it. > >> > >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> wrote: > >>> > >>> This is very interesting. Does it mean that the (oo,1)-category > >>> presented by this model category of cartesian cubical sets is a > >>> (complete and cocomplete) elementary (oo,1)-topos that is not a > >>> Grothendieck (oo,1)-topos? > >>> > >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand > >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote: > >>>> The attached note contains two connected results: > >>>> > >>>> (1) a concrete description of the trivial cofibration-fibration > >>>> factorisation for cartesian > >>>> cubical sets > >>>> > >>>> It follows from this using results of section 2 of Christian Sattler’s > >>>> paper > >>>> > >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911> > >>>> > >>>> that we have a model structure on cartesian cubical sets (that we can call > >>>> “type-theoretic” > >>>> since it is built on ideas coming from type theory), which can be done in a > >>>> constructive > >>>> setting. The fibrant objects of this model structure form a model of type > >>>> theory with universes > >>>> (and conversely the fact that we have a fibrant universe is a crucial > >>>> component in the proof > >>>> that we have a model structure). > >>>> > >>>> I described essentially the same argument for factorisation in a message > >>>> to this list last year > >>>> July 6, 2017 (for another notion of cubical sets however): no quotient > >>>> operation is involved > >>>> in contrast with the "small object argument”. > >>>> This kind of factorisation has been described in a more general framework > >>>> in the paper of Andrew Swan > >>>> > >>>> https://arxiv.org/abs/1802.07588 <https://arxiv.org/abs/1802.07588> > >>>> > >>>> > >>>> > >>>> Since there is a canonical geometric realisation of cartesian cubical sets > >>>> (realising the formal > >>>> interval as the real unit interval [0,1]) a natural question is if this is a > >>>> Quillen equivalence. > >>>> The second result, due to Christian Sattler, is that > >>>> > >>>> (2) the geometric realisation map is -not- a Quillen equivalence. > >>>> > >>>> I believe that this result should be relevant even for people interested in > >>>> the more syntactic > >>>> aspects of type theory. It implies that if we extend cartesian cubical type > >>>> theory > >>>> with a type which is a HIT built from a primitive symmetric square q(x,y) = > >>>> q(y,z), we get a type > >>>> which should be contractible (at least its geometric realisation is) but we > >>>> cannot show this in > >>>> cartesian cubical type theory. > >>>> > >>>> It is thus important to understand better what is going on, and this is why > >>>> I post this note, > >>>> The point (2) is only a concrete description of Sattler’s argument he > >>>> presented last week at the HIM > >>>> meeting. Ulrik Buchholtz has (independently) > >>>> more abstract proofs of similar results (not for cartesian cubical sets > >>>> however), which should bring > >>>> further lights on this question. > >>>> > >>>> Note that this implies that the canonical map Cartesian cubes -> Dedekind > >>>> cubes (corresponding > >>>> to distributive lattices) is also not a Quillen equivalence (for their > >>>> respective type theoretic model > >>>> structures). Hence, as noted by Steve, this implies that the model structure > >>>> obtained by transfer > >>>> and described at > >>>> > >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf <https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf> > >>>> > >>>> is not equivalent to the type-theoretic model structure. > >>>> > >>>> Thierry > >>>> > >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions > >>>> about this last week in Bonn. > >>>> > >>>> -- > >>>> 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:HomotopyTypeTheo...@googlegroups.com>. > >>>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. > >>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout <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: 16396 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 10:27 ` Steve Awodey @ 2018-06-14 13:44 ` Steve Awodey 2018-06-14 14:52 ` Christian Sattler 2018-06-14 15:47 ` Michael Shulman 0 siblings, 2 replies; 21+ messages in thread From: Steve Awodey @ 2018-06-14 13:44 UTC (permalink / raw) To: Christian Sattler; +Cc: Michael Shulman, Thierry Coquand, Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 9849 bytes --] Ok, I think I see what you are saying: we can generate an *algebraic wfs* using the generators I gave previously (regarded as a *category*, with pullback squares of monos, etc., as arrows), and then take the underlying (non-algebraic) wfs by closing under retracts, as usual, and the result is then cofibrantly generated by the *set* of maps you are describing, which consists of quotients of the original ones. generators aside, the cofibrations are all the monos, and the fibrations have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed family of monos, d : I —> I x I is regarded as a generic point of I over I, and the pushout-product m xo d : I^n +_A (A x I) >—> B x I is formed over I as previously described. yes? Steve > On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu> wrote: > > > >> On Jun 14, 2018, at 11:58 AM, Christian Sattler <sattler....@gmail.com <mailto:sattler....@gmail.com>> wrote: >> >> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: >> but they are cofibrantly generated: >> >> - the cofibrations can be taken to be all monos (say), which are generated by subobjects of cubes as usual, and >> >> - the trivial cofibrations are generated by certain subobjects U >—> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, a small set of generating trivial cofibrations. >> >> Those would be the objects of a category of algebraic generators. For generators of the underlying weak factorization systems, one would take any cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, > > this determines the same class of cofibrations as simply taking *all* subobjects of representables, which is already a set. There is no reason to act by Aut(n), etc., here. > >> and for trivial cofibrations the corresponding generators Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. > > sorry, I can’t read your notation. > > the generating trivial cofibrations I stated are the following: > > take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we can also regard as a mono over I by composition with j. Over I we also have the generic point d : I —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I . Then we forget the indexing over I to end up with the description I already gave, namely: > > U = I^n +_A (A x I) > > where the indexing j is built into the pushout over A. > > A more direct description is this: > > let h : I^n —> I^n x I be the graph of j, > let g : A —> A x I be the graph of j.m, > there is a commutative square: > > g > A —— > A x I > | | > m | | m x I > | | > v v > I^n ——> I^n x I > | h > j | > v > I > > put the usual pushout U = I^n +_A (A x I) inside it, > and the comprison map U —> I^n x I is the m xo d mentioned above. > > Steve > > > > > >> >> >> Steve >> >> > >> > 3. They might be a Grothendieck (oo,1)-topos after all. >> > >> > I don't know which of these is most likely; they all seem strange. >> > >> >> > >> > >> > >> > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: >> >> oh, interesting! >> >> because it’s not defined over sSet, but is covered by it. >> >> >> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> wrote: >> >>> >> >>> This is very interesting. Does it mean that the (oo,1)-category >> >>> presented by this model category of cartesian cubical sets is a >> >>> (complete and cocomplete) elementary (oo,1)-topos that is not a >> >>> Grothendieck (oo,1)-topos? >> >>> >> >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >> >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote: >> >>>> The attached note contains two connected results: >> >>>> >> >>>> (1) a concrete description of the trivial cofibration-fibration >> >>>> factorisation for cartesian >> >>>> cubical sets >> >>>> >> >>>> It follows from this using results of section 2 of Christian Sattler’s >> >>>> paper >> >>>> >> >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911> >> >>>> >> >>>> that we have a model structure on cartesian cubical sets (that we can call >> >>>> “type-theoretic” >> >>>> since it is built on ideas coming from type theory), which can be done in a >> >>>> constructive >> >>>> setting. The fibrant objects of this model structure form a model of type >> >>>> theory with universes >> >>>> (and conversely the fact that we have a fibrant universe is a crucial >> >>>> component in the proof >> >>>> that we have a model structure). >> >>>> >> >>>> I described essentially the same argument for factorisation in a message >> >>>> to this list last year >> >>>> July 6, 2017 (for another notion of cubical sets however): no quotient >> >>>> operation is involved >> >>>> in contrast with the "small object argument”. >> >>>> This kind of factorisation has been described in a more general framework >> >>>> in the paper of Andrew Swan >> >>>> >> >>>> https://arxiv.org/abs/1802.07588 <https://arxiv.org/abs/1802.07588> >> >>>> >> >>>> >> >>>> >> >>>> Since there is a canonical geometric realisation of cartesian cubical sets >> >>>> (realising the formal >> >>>> interval as the real unit interval [0,1]) a natural question is if this is a >> >>>> Quillen equivalence. >> >>>> The second result, due to Christian Sattler, is that >> >>>> >> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >> >>>> >> >>>> I believe that this result should be relevant even for people interested in >> >>>> the more syntactic >> >>>> aspects of type theory. It implies that if we extend cartesian cubical type >> >>>> theory >> >>>> with a type which is a HIT built from a primitive symmetric square q(x,y) = >> >>>> q(y,z), we get a type >> >>>> which should be contractible (at least its geometric realisation is) but we >> >>>> cannot show this in >> >>>> cartesian cubical type theory. >> >>>> >> >>>> It is thus important to understand better what is going on, and this is why >> >>>> I post this note, >> >>>> The point (2) is only a concrete description of Sattler’s argument he >> >>>> presented last week at the HIM >> >>>> meeting. Ulrik Buchholtz has (independently) >> >>>> more abstract proofs of similar results (not for cartesian cubical sets >> >>>> however), which should bring >> >>>> further lights on this question. >> >>>> >> >>>> Note that this implies that the canonical map Cartesian cubes -> Dedekind >> >>>> cubes (corresponding >> >>>> to distributive lattices) is also not a Quillen equivalence (for their >> >>>> respective type theoretic model >> >>>> structures). Hence, as noted by Steve, this implies that the model structure >> >>>> obtained by transfer >> >>>> and described at >> >>>> >> >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf <https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf> >> >>>> >> >>>> is not equivalent to the type-theoretic model structure. >> >>>> >> >>>> Thierry >> >>>> >> >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >> >>>> about this last week in Bonn. >> >>>> >> >>>> -- >> >>>> 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:HomotopyTypeTheo...@googlegroups.com>. >> >>>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. >> >>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. >> For more options, visit https://groups.google.com/d/optout <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>. > > > -- > 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: 18968 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 13:44 ` Steve Awodey @ 2018-06-14 14:52 ` Christian Sattler 2018-06-14 15:42 ` Steve Awodey 2018-06-14 15:47 ` Michael Shulman 1 sibling, 1 reply; 21+ messages in thread From: Christian Sattler @ 2018-06-14 14:52 UTC (permalink / raw) To: Steve Awodey; +Cc: Michael Shulman, Thierry Coquand, Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 9422 bytes --] On Thu, Jun 14, 2018 at 3:44 PM, Steve Awodey <awo...@cmu.edu> wrote: > Ok, I think I see what you are saying: > > we can generate an *algebraic wfs* using the generators I gave previously > (regarded as a *category*, with pullback squares of monos, etc., as > arrows), and then take the underlying (non-algebraic) wfs by closing under > retracts, as usual, and the result is then cofibrantly generated by the > *set* of maps you are describing, which consists of quotients of the > original ones. > > generators aside, the cofibrations are all the monos, and the fibrations > have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m > : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed > family of monos, d : I —> I x I is regarded as a generic point of I over I, > and the pushout-product > > m xo d : I^n +_A (A x I) >—> B x I > > is formed over I as previously described. > > yes? > Yes, that's correct. > > Steve > > > On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu> wrote: > > > > On Jun 14, 2018, at 11:58 AM, Christian Sattler < > sattler....@gmail.com> wrote: > > On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote: > >> but they are cofibrantly generated: >> >> - the cofibrations can be taken to be all monos (say), which are >> generated by subobjects of cubes as usual, and >> >> - the trivial cofibrations are generated by certain subobjects U >—> >> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for >> all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, >> a small set of generating trivial cofibrations. >> > > Those would be the objects of a category of algebraic generators. For > generators of the underlying weak factorization systems, one would take any > cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ > Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, > > > this determines the same class of cofibrations as simply taking *all* > subobjects of representables, which is already a set. There is no reason > to act by Aut(n), etc., here. > > and for trivial cofibrations the corresponding generators Σ_I (S_{/I} > hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G > +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. > > > sorry, I can’t read your notation. > > the generating trivial cofibrations I stated are the following: > > take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we > can also regard as a mono over I by composition with j. Over I we also > have the generic point d : I —> I x I , so we can make a push-out product > of d and m over I , say m xo d : U >—> I^n x I . Then we forget the > indexing over I to end up with the description I already gave, namely: > > U = I^n +_A (A x I) > > where the indexing j is built into the pushout over A. > > A more direct description is this: > > let h : I^n —> I^n x I be the graph of j, > let g : A —> A x I be the graph of j.m, > there is a commutative square: > > g > A —— > A x I > | | > m | | m x I > | | > v v > I^n ——> I^n x I > | h > j | > v > I > > put the usual pushout U = I^n +_A (A x I) inside it, > and the comprison map U —> I^n x I is the m xo d mentioned above. > > Steve > > > > > > > >> Steve >> >> > >> > 3. They might be a Grothendieck (oo,1)-topos after all. >> > >> > I don't know which of these is most likely; they all seem strange. >> > >> >> > >> > >> > >> > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: >> >> oh, interesting! >> >> because it’s not defined over sSet, but is covered by it. >> >> >> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> >> wrote: >> >>> >> >>> This is very interesting. Does it mean that the (oo,1)-category >> >>> presented by this model category of cartesian cubical sets is a >> >>> (complete and cocomplete) elementary (oo,1)-topos that is not a >> >>> Grothendieck (oo,1)-topos? >> >>> >> >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >> >>> <Thierry...@cse.gu.se> wrote: >> >>>> The attached note contains two connected results: >> >>>> >> >>>> (1) a concrete description of the trivial cofibration-fibration >> >>>> factorisation for cartesian >> >>>> cubical sets >> >>>> >> >>>> It follows from this using results of section 2 of Christian >> Sattler’s >> >>>> paper >> >>>> >> >>>> https://arxiv.org/pdf/1704.06911 >> >>>> >> >>>> that we have a model structure on cartesian cubical sets (that we >> can call >> >>>> “type-theoretic” >> >>>> since it is built on ideas coming from type theory), which can be >> done in a >> >>>> constructive >> >>>> setting. The fibrant objects of this model structure form a model of >> type >> >>>> theory with universes >> >>>> (and conversely the fact that we have a fibrant universe is a crucial >> >>>> component in the proof >> >>>> that we have a model structure). >> >>>> >> >>>> I described essentially the same argument for factorisation in a >> message >> >>>> to this list last year >> >>>> July 6, 2017 (for another notion of cubical sets however): no >> quotient >> >>>> operation is involved >> >>>> in contrast with the "small object argument”. >> >>>> This kind of factorisation has been described in a more general >> framework >> >>>> in the paper of Andrew Swan >> >>>> >> >>>> https://arxiv.org/abs/1802.07588 >> >>>> >> >>>> >> >>>> >> >>>> Since there is a canonical geometric realisation of cartesian >> cubical sets >> >>>> (realising the formal >> >>>> interval as the real unit interval [0,1]) a natural question is if >> this is a >> >>>> Quillen equivalence. >> >>>> The second result, due to Christian Sattler, is that >> >>>> >> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >> >>>> >> >>>> I believe that this result should be relevant even for people >> interested in >> >>>> the more syntactic >> >>>> aspects of type theory. It implies that if we extend cartesian >> cubical type >> >>>> theory >> >>>> with a type which is a HIT built from a primitive symmetric square >> q(x,y) = >> >>>> q(y,z), we get a type >> >>>> which should be contractible (at least its geometric realisation is) >> but we >> >>>> cannot show this in >> >>>> cartesian cubical type theory. >> >>>> >> >>>> It is thus important to understand better what is going on, and this >> is why >> >>>> I post this note, >> >>>> The point (2) is only a concrete description of Sattler’s argument he >> >>>> presented last week at the HIM >> >>>> meeting. Ulrik Buchholtz has (independently) >> >>>> more abstract proofs of similar results (not for cartesian cubical >> sets >> >>>> however), which should bring >> >>>> further lights on this question. >> >>>> >> >>>> Note that this implies that the canonical map Cartesian cubes -> >> Dedekind >> >>>> cubes (corresponding >> >>>> to distributive lattices) is also not a Quillen equivalence (for >> their >> >>>> respective type theoretic model >> >>>> structures). Hence, as noted by Steve, this implies that the model >> structure >> >>>> obtained by transfer >> >>>> and described at >> >>>> >> >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >> >>>> >> >>>> is not equivalent to the type-theoretic model structure. >> >>>> >> >>>> Thierry >> >>>> >> >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for >> discussions >> >>>> about this last week in Bonn. >> >>>> >> >>>> -- >> >>>> 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: 17754 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 14:52 ` Christian Sattler @ 2018-06-14 15:42 ` Steve Awodey 0 siblings, 0 replies; 21+ messages in thread From: Steve Awodey @ 2018-06-14 15:42 UTC (permalink / raw) To: Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 9785 bytes --] 1 correction: > generators aside, the cofibrations are all the monos, and the fibrations have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed family of monos, d : I —> I x I is regarded as a generic point of I over I, and the pushout-product > > m xo d : I^n +_A (A x I) >—> B x I should be: m xo d : B +_A (A x I) >—> B x I Steve > > is formed over I as previously described. > > yes? > > Yes, that's correct. > > > Steve > > >> On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: >> >> >> >>> On Jun 14, 2018, at 11:58 AM, Christian Sattler <sattler....@gmail.com <mailto:sattler....@gmail.com>> wrote: >>> >>> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: >>> but they are cofibrantly generated: >>> >>> - the cofibrations can be taken to be all monos (say), which are generated by subobjects of cubes as usual, and >>> >>> - the trivial cofibrations are generated by certain subobjects U >—> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, a small set of generating trivial cofibrations. >>> >>> Those would be the objects of a category of algebraic generators. For generators of the underlying weak factorization systems, one would take any cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, >> >> this determines the same class of cofibrations as simply taking *all* subobjects of representables, which is already a set. There is no reason to act by Aut(n), etc., here. >> >>> and for trivial cofibrations the corresponding generators Σ_I (S_{/I} hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. >> >> sorry, I can’t read your notation. >> >> the generating trivial cofibrations I stated are the following: >> >> take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we can also regard as a mono over I by composition with j. Over I we also have the generic point d : I —> I x I , so we can make a push-out product of d and m over I , say m xo d : U >—> I^n x I . Then we forget the indexing over I to end up with the description I already gave, namely: >> >> U = I^n +_A (A x I) >> >> where the indexing j is built into the pushout over A. >> >> A more direct description is this: >> >> let h : I^n —> I^n x I be the graph of j, >> let g : A —> A x I be the graph of j.m, >> there is a commutative square: >> >> g >> A —— > A x I >> | | >> m | | m x I >> | | >> v v >> I^n ——> I^n x I >> | h >> j | >> v >> I >> >> put the usual pushout U = I^n +_A (A x I) inside it, >> and the comprison map U —> I^n x I is the m xo d mentioned above. >> >> Steve >> >> >> >> >> >>> >>> >>> Steve >>> >>> > >>> > 3. They might be a Grothendieck (oo,1)-topos after all. >>> > >>> > I don't know which of these is most likely; they all seem strange. >>> > >>> >>> > >>> > >>> > >>> > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote: >>> >> oh, interesting! >>> >> because it’s not defined over sSet, but is covered by it. >>> >> >>> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu <mailto:shu...@sandiego.edu>> wrote: >>> >>> >>> >>> This is very interesting. Does it mean that the (oo,1)-category >>> >>> presented by this model category of cartesian cubical sets is a >>> >>> (complete and cocomplete) elementary (oo,1)-topos that is not a >>> >>> Grothendieck (oo,1)-topos? >>> >>> >>> >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >>> >>> <Thierry...@cse.gu.se <mailto:Thierry...@cse.gu.se>> wrote: >>> >>>> The attached note contains two connected results: >>> >>>> >>> >>>> (1) a concrete description of the trivial cofibration-fibration >>> >>>> factorisation for cartesian >>> >>>> cubical sets >>> >>>> >>> >>>> It follows from this using results of section 2 of Christian Sattler’s >>> >>>> paper >>> >>>> >>> >>>> https://arxiv.org/pdf/1704.06911 <https://arxiv.org/pdf/1704.06911> >>> >>>> >>> >>>> that we have a model structure on cartesian cubical sets (that we can call >>> >>>> “type-theoretic” >>> >>>> since it is built on ideas coming from type theory), which can be done in a >>> >>>> constructive >>> >>>> setting. The fibrant objects of this model structure form a model of type >>> >>>> theory with universes >>> >>>> (and conversely the fact that we have a fibrant universe is a crucial >>> >>>> component in the proof >>> >>>> that we have a model structure). >>> >>>> >>> >>>> I described essentially the same argument for factorisation in a message >>> >>>> to this list last year >>> >>>> July 6, 2017 (for another notion of cubical sets however): no quotient >>> >>>> operation is involved >>> >>>> in contrast with the "small object argument”. >>> >>>> This kind of factorisation has been described in a more general framework >>> >>>> in the paper of Andrew Swan >>> >>>> >>> >>>> https://arxiv.org/abs/1802.07588 <https://arxiv.org/abs/1802.07588> >>> >>>> >>> >>>> >>> >>>> >>> >>>> Since there is a canonical geometric realisation of cartesian cubical sets >>> >>>> (realising the formal >>> >>>> interval as the real unit interval [0,1]) a natural question is if this is a >>> >>>> Quillen equivalence. >>> >>>> The second result, due to Christian Sattler, is that >>> >>>> >>> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>> >>>> >>> >>>> I believe that this result should be relevant even for people interested in >>> >>>> the more syntactic >>> >>>> aspects of type theory. It implies that if we extend cartesian cubical type >>> >>>> theory >>> >>>> with a type which is a HIT built from a primitive symmetric square q(x,y) = >>> >>>> q(y,z), we get a type >>> >>>> which should be contractible (at least its geometric realisation is) but we >>> >>>> cannot show this in >>> >>>> cartesian cubical type theory. >>> >>>> >>> >>>> It is thus important to understand better what is going on, and this is why >>> >>>> I post this note, >>> >>>> The point (2) is only a concrete description of Sattler’s argument he >>> >>>> presented last week at the HIM >>> >>>> meeting. Ulrik Buchholtz has (independently) >>> >>>> more abstract proofs of similar results (not for cartesian cubical sets >>> >>>> however), which should bring >>> >>>> further lights on this question. >>> >>>> >>> >>>> Note that this implies that the canonical map Cartesian cubes -> Dedekind >>> >>>> cubes (corresponding >>> >>>> to distributive lattices) is also not a Quillen equivalence (for their >>> >>>> respective type theoretic model >>> >>>> structures). Hence, as noted by Steve, this implies that the model structure >>> >>>> obtained by transfer >>> >>>> and described at >>> >>>> >>> >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf <https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf> >>> >>>> >>> >>>> is not equivalent to the type-theoretic model structure. >>> >>>> >>> >>>> Thierry >>> >>>> >>> >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for discussions >>> >>>> about this last week in Bonn. >>> >>>> >>> >>>> -- >>> >>>> 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:HomotopyTypeTheo...@googlegroups.com>. >>> >>>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. >>> >>> For more options, visit https://groups.google.com/d/optout <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:HomotopyTypeTheo...@googlegroups.com>. >>> For more options, visit https://groups.google.com/d/optout <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>. >> >> >> -- >> 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: 20848 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 13:44 ` Steve Awodey 2018-06-14 14:52 ` Christian Sattler @ 2018-06-14 15:47 ` Michael Shulman 2018-06-14 16:01 ` Steve Awodey 1 sibling, 1 reply; 21+ messages in thread From: Michael Shulman @ 2018-06-14 15:47 UTC (permalink / raw) To: Steve Awodey; +Cc: Christian Sattler, Thierry Coquand, Homotopy Theory Okay, if the non-algebraic wfs's are cofibrantly generated in the traditional sense, then the model category is indeed combinatorial. Christian has also pointed out by private email that for a locally presentable, locally cartesian closed (oo,1)-category (and, I think, even any cocomplete locally cartesian closed one) the infinitary aspects of the Giraud exactness axioms follow from finitary ones (for roughly the same reasons as in the 1-categorical case) --- specifically the "van Kampen" nature of pushouts, which should be provable in any elementary (oo,1)-topos and thus presumably in cartesian cubical sets. So it seems that it's my possibility (3) that holds -- this model structure does present a Grothendieck (oo,1)-topos. We should be able to work out a more traditional description of it as a left exact localization of some (oo,1)-presheaf category by tracing through the proofs of the presentation theorem and Giraud's theorem. On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey <awo...@cmu.edu> wrote: > Ok, I think I see what you are saying: > > we can generate an *algebraic wfs* using the generators I gave previously > (regarded as a *category*, with pullback squares of monos, etc., as arrows), > and then take the underlying (non-algebraic) wfs by closing under retracts, > as usual, and the result is then cofibrantly generated by the *set* of maps > you are describing, which consists of quotients of the original ones. > > generators aside, the cofibrations are all the monos, and the fibrations > have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m > : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed > family of monos, d : I —> I x I is regarded as a generic point of I over I, > and the pushout-product > > m xo d : I^n +_A (A x I) >—> B x I > > is formed over I as previously described. > > yes? > > Steve > > > On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu> wrote: > > > > On Jun 14, 2018, at 11:58 AM, Christian Sattler > <sattler....@gmail.com> wrote: > > On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote: >> >> but they are cofibrantly generated: >> >> - the cofibrations can be taken to be all monos (say), which are generated >> by subobjects of cubes as usual, and >> >> - the trivial cofibrations are generated by certain subobjects U >—> >> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for >> all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, >> a small set of generating trivial cofibrations. > > > Those would be the objects of a category of algebraic generators. For > generators of the underlying weak factorization systems, one would take any > cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ > Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, > > > this determines the same class of cofibrations as simply taking *all* > subobjects of representables, which is already a set. There is no reason to > act by Aut(n), etc., here. > > and for trivial cofibrations the corresponding generators Σ_I (S_{/I} > hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. > □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. > > > sorry, I can’t read your notation. > > the generating trivial cofibrations I stated are the following: > > take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we can > also regard as a mono over I by composition with j. Over I we also have the > generic point d : I —> I x I , so we can make a push-out product of d and m > over I , say m xo d : U >—> I^n x I . Then we forget the indexing over I to > end up with the description I already gave, namely: > > U = I^n +_A (A x I) > > where the indexing j is built into the pushout over A. > > A more direct description is this: > > let h : I^n —> I^n x I be the graph of j, > let g : A —> A x I be the graph of j.m, > there is a commutative square: > > g > A —— > A x I > | | > m | | m x I > | | > v v > I^n ——> I^n x I > | h > j | > v > I > > put the usual pushout U = I^n +_A (A x I) inside it, > and the comprison map U —> I^n x I is the m xo d mentioned above. > > Steve > > > > > > >> >> Steve >> >> > >> > 3. They might be a Grothendieck (oo,1)-topos after all. >> > >> > I don't know which of these is most likely; they all seem strange. >> > >> >> > >> > >> > >> > On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: >> >> oh, interesting! >> >> because it’s not defined over sSet, but is covered by it. >> >> >> >>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> >> >>> wrote: >> >>> >> >>> This is very interesting. Does it mean that the (oo,1)-category >> >>> presented by this model category of cartesian cubical sets is a >> >>> (complete and cocomplete) elementary (oo,1)-topos that is not a >> >>> Grothendieck (oo,1)-topos? >> >>> >> >>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >> >>> <Thierry...@cse.gu.se> wrote: >> >>>> The attached note contains two connected results: >> >>>> >> >>>> (1) a concrete description of the trivial cofibration-fibration >> >>>> factorisation for cartesian >> >>>> cubical sets >> >>>> >> >>>> It follows from this using results of section 2 of Christian >> >>>> Sattler’s >> >>>> paper >> >>>> >> >>>> https://arxiv.org/pdf/1704.06911 >> >>>> >> >>>> that we have a model structure on cartesian cubical sets (that we can >> >>>> call >> >>>> “type-theoretic” >> >>>> since it is built on ideas coming from type theory), which can be >> >>>> done in a >> >>>> constructive >> >>>> setting. The fibrant objects of this model structure form a model of >> >>>> type >> >>>> theory with universes >> >>>> (and conversely the fact that we have a fibrant universe is a crucial >> >>>> component in the proof >> >>>> that we have a model structure). >> >>>> >> >>>> I described essentially the same argument for factorisation in a >> >>>> message >> >>>> to this list last year >> >>>> July 6, 2017 (for another notion of cubical sets however): no >> >>>> quotient >> >>>> operation is involved >> >>>> in contrast with the "small object argument”. >> >>>> This kind of factorisation has been described in a more general >> >>>> framework >> >>>> in the paper of Andrew Swan >> >>>> >> >>>> https://arxiv.org/abs/1802.07588 >> >>>> >> >>>> >> >>>> >> >>>> Since there is a canonical geometric realisation of cartesian cubical >> >>>> sets >> >>>> (realising the formal >> >>>> interval as the real unit interval [0,1]) a natural question is if >> >>>> this is a >> >>>> Quillen equivalence. >> >>>> The second result, due to Christian Sattler, is that >> >>>> >> >>>> (2) the geometric realisation map is -not- a Quillen equivalence. >> >>>> >> >>>> I believe that this result should be relevant even for people >> >>>> interested in >> >>>> the more syntactic >> >>>> aspects of type theory. It implies that if we extend cartesian >> >>>> cubical type >> >>>> theory >> >>>> with a type which is a HIT built from a primitive symmetric square >> >>>> q(x,y) = >> >>>> q(y,z), we get a type >> >>>> which should be contractible (at least its geometric realisation is) >> >>>> but we >> >>>> cannot show this in >> >>>> cartesian cubical type theory. >> >>>> >> >>>> It is thus important to understand better what is going on, and this >> >>>> is why >> >>>> I post this note, >> >>>> The point (2) is only a concrete description of Sattler’s argument he >> >>>> presented last week at the HIM >> >>>> meeting. Ulrik Buchholtz has (independently) >> >>>> more abstract proofs of similar results (not for cartesian cubical >> >>>> sets >> >>>> however), which should bring >> >>>> further lights on this question. >> >>>> >> >>>> Note that this implies that the canonical map Cartesian cubes -> >> >>>> Dedekind >> >>>> cubes (corresponding >> >>>> to distributive lattices) is also not a Quillen equivalence (for >> >>>> their >> >>>> respective type theoretic model >> >>>> structures). Hence, as noted by Steve, this implies that the model >> >>>> structure >> >>>> obtained by transfer >> >>>> and described at >> >>>> >> >>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >> >>>> >> >>>> is not equivalent to the type-theoretic model structure. >> >>>> >> >>>> Thierry >> >>>> >> >>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for >> >>>> discussions >> >>>> about this last week in Bonn. >> >>>> >> >>>> -- >> >>>> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 15:47 ` Michael Shulman @ 2018-06-14 16:01 ` Steve Awodey 0 siblings, 0 replies; 21+ messages in thread From: Steve Awodey @ 2018-06-14 16:01 UTC (permalink / raw) To: Michael Shulman; +Cc: Christian Sattler, Thierry Coquand, Homotopy Theory > On Jun 14, 2018, at 5:47 PM, Michael Shulman <shu...@sandiego.edu> wrote: > > Okay, if the non-algebraic wfs's are cofibrantly generated in the > traditional sense, then the model category is indeed combinatorial. > Christian has also pointed out by private email that for a locally > presentable, locally cartesian closed (oo,1)-category (and, I think, > even any cocomplete locally cartesian closed one) the infinitary > aspects of the Giraud exactness axioms follow from finitary ones (for > roughly the same reasons as in the 1-categorical case) --- > specifically the "van Kampen" nature of pushouts, which should be > provable in any elementary (oo,1)-topos and thus presumably in > cartesian cubical sets. > > So it seems that it's my possibility (3) that holds -- this model > structure does present a Grothendieck (oo,1)-topos. We should be able > to work out a more traditional description of it as a left exact > localization of some (oo,1)-presheaf category by tracing through the > proofs of the presentation theorem and Giraud's theorem. > a formidable task … and a good open problem! thanks for clarifying. Steve > > On Thu, Jun 14, 2018 at 6:44 AM, Steve Awodey <awo...@cmu.edu> wrote: >> Ok, I think I see what you are saying: >> >> we can generate an *algebraic wfs* using the generators I gave previously >> (regarded as a *category*, with pullback squares of monos, etc., as arrows), >> and then take the underlying (non-algebraic) wfs by closing under retracts, >> as usual, and the result is then cofibrantly generated by the *set* of maps >> you are describing, which consists of quotients of the original ones. >> >> generators aside, the cofibrations are all the monos, and the fibrations >> have the RLP w/resp. to all push-out products m xo d : U >—> B x I, where m >> : A >—> B is any mono, j : B —> I is some indexing making m an I-indexed >> family of monos, d : I —> I x I is regarded as a generic point of I over I, >> and the pushout-product >> >> m xo d : I^n +_A (A x I) >—> B x I >> >> is formed over I as previously described. >> >> yes? >> >> Steve >> >> >> On Jun 14, 2018, at 12:27 PM, Steve Awodey <awo...@cmu.edu> wrote: >> >> >> >> On Jun 14, 2018, at 11:58 AM, Christian Sattler >> <sattler....@gmail.com> wrote: >> >> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote: >>> >>> but they are cofibrantly generated: >>> >>> - the cofibrations can be taken to be all monos (say), which are generated >>> by subobjects of cubes as usual, and >>> >>> - the trivial cofibrations are generated by certain subobjects U >—> >>> I^{n+1} , where the U are pushout-products of the form I^n +_A (A x I) for >>> all A >—> I^n cofibrant and there is some indexing I^n —> I . In any case, >>> a small set of generating trivial cofibrations. >> >> >> Those would be the objects of a category of algebraic generators. For >> generators of the underlying weak factorization systems, one would take any >> cellular model S of monomorphisms, here for example ∂□ⁿ/G → □ⁿ/G where G ⊆ >> Aut(□ⁿ) and ∂□ⁿ denotes the maximal no-trivial subobject, >> >> >> this determines the same class of cofibrations as simply taking *all* >> subobjects of representables, which is already a set. There is no reason to >> act by Aut(n), etc., here. >> >> and for trivial cofibrations the corresponding generators Σ_I (S_{/I} >> hat(×)_{/I} d) with d : I → I² the diagonal (seen as living over I), i.e. >> □ⁿ/G +_{∂□ⁿ/G} I × ∂□ⁿ/G → I × □ⁿ/G for all n, G, and □ⁿ/G → I. >> >> >> sorry, I can’t read your notation. >> >> the generating trivial cofibrations I stated are the following: >> >> take any “indexing” map j : I^n —> I and a mono m : A >—> I^n, which we can >> also regard as a mono over I by composition with j. Over I we also have the >> generic point d : I —> I x I , so we can make a push-out product of d and m >> over I , say m xo d : U >—> I^n x I . Then we forget the indexing over I to >> end up with the description I already gave, namely: >> >> U = I^n +_A (A x I) >> >> where the indexing j is built into the pushout over A. >> >> A more direct description is this: >> >> let h : I^n —> I^n x I be the graph of j, >> let g : A —> A x I be the graph of j.m, >> there is a commutative square: >> >> g >> A —— > A x I >> | | >> m | | m x I >> | | >> v v >> I^n ——> I^n x I >> | h >> j | >> v >> I >> >> put the usual pushout U = I^n +_A (A x I) inside it, >> and the comprison map U —> I^n x I is the m xo d mentioned above. >> >> Steve >> >> >> >> >> >> >>> >>> Steve >>> >>>> >>>> 3. They might be a Grothendieck (oo,1)-topos after all. >>>> >>>> I don't know which of these is most likely; they all seem strange. >>>> >>> >>>> >>>> >>>> >>>> On Wed, Jun 13, 2018 at 1:50 PM, Steve Awodey <awo...@cmu.edu> wrote: >>>>> oh, interesting! >>>>> because it’s not defined over sSet, but is covered by it. >>>>> >>>>>> On Jun 13, 2018, at 10:33 PM, Michael Shulman <shu...@sandiego.edu> >>>>>> wrote: >>>>>> >>>>>> This is very interesting. Does it mean that the (oo,1)-category >>>>>> presented by this model category of cartesian cubical sets is a >>>>>> (complete and cocomplete) elementary (oo,1)-topos that is not a >>>>>> Grothendieck (oo,1)-topos? >>>>>> >>>>>> On Sun, Jun 10, 2018 at 6:31 AM, Thierry Coquand >>>>>> <Thierry...@cse.gu.se> wrote: >>>>>>> The attached note contains two connected results: >>>>>>> >>>>>>> (1) a concrete description of the trivial cofibration-fibration >>>>>>> factorisation for cartesian >>>>>>> cubical sets >>>>>>> >>>>>>> It follows from this using results of section 2 of Christian >>>>>>> Sattler’s >>>>>>> paper >>>>>>> >>>>>>> https://arxiv.org/pdf/1704.06911 >>>>>>> >>>>>>> that we have a model structure on cartesian cubical sets (that we can >>>>>>> call >>>>>>> “type-theoretic” >>>>>>> since it is built on ideas coming from type theory), which can be >>>>>>> done in a >>>>>>> constructive >>>>>>> setting. The fibrant objects of this model structure form a model of >>>>>>> type >>>>>>> theory with universes >>>>>>> (and conversely the fact that we have a fibrant universe is a crucial >>>>>>> component in the proof >>>>>>> that we have a model structure). >>>>>>> >>>>>>> I described essentially the same argument for factorisation in a >>>>>>> message >>>>>>> to this list last year >>>>>>> July 6, 2017 (for another notion of cubical sets however): no >>>>>>> quotient >>>>>>> operation is involved >>>>>>> in contrast with the "small object argument”. >>>>>>> This kind of factorisation has been described in a more general >>>>>>> framework >>>>>>> in the paper of Andrew Swan >>>>>>> >>>>>>> https://arxiv.org/abs/1802.07588 >>>>>>> >>>>>>> >>>>>>> >>>>>>> Since there is a canonical geometric realisation of cartesian cubical >>>>>>> sets >>>>>>> (realising the formal >>>>>>> interval as the real unit interval [0,1]) a natural question is if >>>>>>> this is a >>>>>>> Quillen equivalence. >>>>>>> The second result, due to Christian Sattler, is that >>>>>>> >>>>>>> (2) the geometric realisation map is -not- a Quillen equivalence. >>>>>>> >>>>>>> I believe that this result should be relevant even for people >>>>>>> interested in >>>>>>> the more syntactic >>>>>>> aspects of type theory. It implies that if we extend cartesian >>>>>>> cubical type >>>>>>> theory >>>>>>> with a type which is a HIT built from a primitive symmetric square >>>>>>> q(x,y) = >>>>>>> q(y,z), we get a type >>>>>>> which should be contractible (at least its geometric realisation is) >>>>>>> but we >>>>>>> cannot show this in >>>>>>> cartesian cubical type theory. >>>>>>> >>>>>>> It is thus important to understand better what is going on, and this >>>>>>> is why >>>>>>> I post this note, >>>>>>> The point (2) is only a concrete description of Sattler’s argument he >>>>>>> presented last week at the HIM >>>>>>> meeting. Ulrik Buchholtz has (independently) >>>>>>> more abstract proofs of similar results (not for cartesian cubical >>>>>>> sets >>>>>>> however), which should bring >>>>>>> further lights on this question. >>>>>>> >>>>>>> Note that this implies that the canonical map Cartesian cubes -> >>>>>>> Dedekind >>>>>>> cubes (corresponding >>>>>>> to distributive lattices) is also not a Quillen equivalence (for >>>>>>> their >>>>>>> respective type theoretic model >>>>>>> structures). Hence, as noted by Steve, this implies that the model >>>>>>> structure >>>>>>> obtained by transfer >>>>>>> and described at >>>>>>> >>>>>>> https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf >>>>>>> >>>>>>> is not equivalent to the type-theoretic model structure. >>>>>>> >>>>>>> Thierry >>>>>>> >>>>>>> PS: Many thanks to Steve, Christian, Ulrik, Nicola and Dan for >>>>>>> discussions >>>>>>> about this last week in Bonn. >>>>>>> >>>>>>> -- >>>>>>> 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-10 13:31 Quillen model structure Thierry Coquand [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com> 2018-06-13 20:33 ` Michael Shulman @ 2018-06-14 18:39 ` Richard Williamson 2018-06-14 19:14 ` Steve Awodey ` (2 more replies) 2 siblings, 3 replies; 21+ messages in thread From: Richard Williamson @ 2018-06-14 18:39 UTC (permalink / raw) To: Thierry Coquand; +Cc: Homotopy Theory Dear Thierry, Forgive me for not quite having an overview of exactly what has been done. My interest here is in how the model structure you have constructed compares with Cisinski's work. For example, I would expect that the category of cartesian cubical sets is a test category. Indeed, I would expect that more or less exactly the same technique as in 8.4 of Les préfaisceaux comme ... goes through to prove this. And I would expect that one can put a model structure on in the same way. Now, I believe I saw in some slides that that your model structure coincides with the Cisinski one. But this does not seem compatible with my expectations above, because then it is certainly Quillen equivalent to the Serre model structure on topological spaces (or whatever). Thus my questions: 1) Have I misinterpreted the slides or some other aspect of your work? 2) If not, where exactly do Cisinski's techniques fail? Best wishes, Richard ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 18:39 ` Richard Williamson @ 2018-06-14 19:14 ` Steve Awodey 2018-06-14 20:15 ` Richard Williamson 2018-06-14 19:16 ` Thierry Coquand 2018-06-14 19:35 ` [HoTT] Quillen model structure, PS Thierry Coquand 2 siblings, 1 reply; 21+ messages in thread From: Steve Awodey @ 2018-06-14 19:14 UTC (permalink / raw) To: Richard Williamson; +Cc: Thierry Coquand, Homotopy Theory Dear Richard, I believe the answer to (1) is yes : - ) The main point of Thierry's note is that the so-called “type theoretic model structure” on cartesian cubical sets (which as Thierry clearly says is essentially the work of Christian Sattler) is *not* equivalent to the one arising from the (well-known) fact that the cartesian cube category is a (strict) test category. Where exactly this conflicts with a Cisinski style approach is a distinct issue, I think — maybe that’s your (2)? Regards, Steve > On Jun 14, 2018, at 8:39 PM, Richard Williamson <rwilli...@gmail.com> wrote: > > Dear Thierry, > > Forgive me for not quite having an overview of exactly what has > been done. My interest here is in how the model structure you > have constructed compares with Cisinski's work. For example, I > would expect that the category of cartesian cubical sets is a > test category. Indeed, I would expect that more or less exactly > the same technique as in 8.4 of Les préfaisceaux comme ... goes > through to prove this. And I would expect that one can put a > model structure on in the same way. > > Now, I believe I saw in some slides that that your model > structure coincides with the Cisinski one. But this does not seem > compatible with my expectations above, because then it is > certainly Quillen equivalent to the Serre model structure on > topological spaces (or whatever). > > Thus my questions: > > 1) Have I misinterpreted the slides or some other aspect of your > work? > > 2) If not, where exactly do Cisinski's techniques fail? > > Best wishes, > Richard > > -- > 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] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 19:14 ` Steve Awodey @ 2018-06-14 20:15 ` Richard Williamson 2018-06-14 20:32 ` Ulrik Buchholtz 2018-06-14 21:07 ` Richard Williamson 0 siblings, 2 replies; 21+ messages in thread From: Richard Williamson @ 2018-06-14 20:15 UTC (permalink / raw) To: Steve Awodey; +Cc: Thierry Coquand, Homotopy Theory Dear Steve and Thierry, > I believe the answer to (1) is yes : - ) Hehe, that is very likely, and I will be happy to acknowledge it! :-) > Where exactly this conflicts with a Cisinski style approach is > a distinct issue, I think — maybe that’s your (2)? Exactly. It has been a little while since I was really working on this stuff, so I could be forgetting something, but as far as I know the test model structure on cartesian cubical sets is exactly the one coming from the theorem of Cisinski that Thierry cites using the obvious cylinder, and with empty S. Now, Thierry also says, I believe, that this model structure is the same as the one of Christian Sattler. How can this be?! Presumably I have something wrong, but I do not see yet what it is after the replies so far. Best wishes, Richard ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 20:15 ` Richard Williamson @ 2018-06-14 20:32 ` Ulrik Buchholtz 2018-06-14 21:07 ` Richard Williamson 1 sibling, 0 replies; 21+ messages in thread From: Ulrik Buchholtz @ 2018-06-14 20:32 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1405 bytes --] > > Exactly. It has been a little while since I was really working on > this stuff, so I could be forgetting something, but as far as I > know the test model structure on cartesian cubical sets is > exactly the one coming from the theorem of Cisinski that Thierry > cites using the obvious cylinder, and with empty S. Now, Thierry > also says, I believe, that this model structure is the same as > the one of Christian Sattler. How can this be?! > The weak equivalences of the test model structure form the least _regular_ test localizer. The identity adjunction gives a left Quillen functor from the type theoretic model structure to the test model structure, but this is only an equivalence when the weak equivalences of the former form a regular localizer (meaning: every presheaf is the homotopy colimit of its category of elements). BTW, for de Morgan (or Kleene) cubes, geometric realization is not even a left Quillen adjunct for the type theoretic model structure with all (decidable) monos as cofibrations, since the geometric realization of the inclusion of the union of the two diagonals into the square is not a topological cofibration (it's not even injective). There are “smaller” type theoretic model structures with fewer cofibrations, but even for those, geometric realization cannot be a Quillen equivalence. Best wishes, Ulrik [-- Attachment #1.2: Type: text/html, Size: 1646 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 20:15 ` Richard Williamson 2018-06-14 20:32 ` Ulrik Buchholtz @ 2018-06-14 21:07 ` Richard Williamson 1 sibling, 0 replies; 21+ messages in thread From: Richard Williamson @ 2018-06-14 21:07 UTC (permalink / raw) To: Steve Awodey; +Cc: Thierry Coquand, Homotopy Theory > Exactly. It has been a little while since I was really working on > this stuff, so I could be forgetting something, but as far as I > know the test model structure on cartesian cubical sets is > exactly the one coming from the theorem of Cisinski that Thierry > cites using the obvious cylinder, and with empty S. Now, Thierry > also says, I believe, that this model structure is the same as > the one of Christian Sattler. How can this be?! I was mis-remembering. If one looks at 8.4.34 - 8.4.38 in Les préfaisceaux ..., one sees that S is taken (of course, now that I think properly about it!) to be the (non-empty!) set of horn inclusions. In summary, the difference, from the point of view of Cisinski's theory, between the type-theoretic model structure and the test model structure seems to be precisely the choice of S. Thank you to all! ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure 2018-06-14 18:39 ` Richard Williamson 2018-06-14 19:14 ` Steve Awodey @ 2018-06-14 19:16 ` Thierry Coquand 2018-06-14 19:35 ` [HoTT] Quillen model structure, PS Thierry Coquand 2 siblings, 0 replies; 21+ messages in thread From: Thierry Coquand @ 2018-06-14 19:16 UTC (permalink / raw) To: Richard Williamson; +Cc: Homotopy Theory [-- Attachment #1: Type: text/plain, Size: 4582 bytes --] Dear Richard, The model structure is not due to me but to Christian Sattler, and is explained in Section 2 of https://arxiv.org/pdf/1704.06911 (where I did some joint work is in the constructive argument that we have fibrant universes). Cisinski defines in his book a model structure on presheaves where cofibrations are monos. In order to define the model structure, one needs a “cylindre fonctoriel” that we can define from a “segment” II (a presheaf with two global distinct elements 0 and 1) Exemple 1.3.8. We further need a “donnee homotopique” Definition 1.3.14, given by a set of monomorphism S. We only consider here the least case where S = empty set. From this we can define a notion of anodyne map. Given II and S, Cisinski explains then how to define a Quillen model structure Theorem 1.3.22 where -the cofibrations are the monomorphism -the anodyne maps are generated by open box inclusion, A x II \cup B x b -> B x II for A -> B mono and b = 0,1 -the fibrant objects are the ones having the extension property w.r.t. anodyne maps -the -naive- fibrations are the maps having the right lifting properties w.r.t. anodyne maps (so a map X -> 1 is a naive fibration iff X if fibrant) -the weak equivalence are the maps A -> B such that for any fibrant X, the map X^B -> X^A is a homotopy equivalence (w.r.t. the choice of the interval II) -the fibrations are the maps having the right lifting properties w.r.t. maps that are monos and weak equivalence W.r.t. the slides at http://uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Coquand-2018-05-24-HoTTEST.pdf if we limit ourselves to the case where the base category is the Lawvere theory of distributive lattices, or de Morgan algebra, or Boolean algebra and we take the fibrations as defined page 13, we get the same notion as Cisinski -naive- fibrations. It follows from Section 2 of Christian’s paper above that we also get a model structure having exactly this notion of fibration (and where cofibrations are monos). We then have a priori two model structures on these presheaves. They have the same notion of fibrant objects and cofibrations. It follows then from André Joyal’s result (Riehl Categorical Model Theory, Theorem 15.3.1) that we actually the -same- model structure. It then follows that in these cases, the Cisinski model structure is -complete- (Definition 1.3.48). In the case of de Morgan algebra, or distributive lattice, we have a geometric realisation map. However in the case of de Morgan algebra, we don’t have that this map is a Quillen equivalence as shown by Christian: if we take L to be the quotient of II by the de Morgan reversal operation then the geometric realisation of L is contractible, but it can be shown that the map L -> 1 is not an equivalence for Cisinski (= Christian in this case) model structure. It is an open problem what happens for distributive lattices. I am not a specialist of test categories but my understanding is that all these categories (Lawvere theory of distributive lattices, de Morgan algebra, algebra with two constants 0,1) are test categories, but it is not clear if the general notion of weak equivalence we get from the theory of test category coincide with the one of Cisinski model structure (and indeed it will not coincide for de Morgan algebra and Boolean algebra, and this is open for distributive lattices), Best regards, Thierry On 14 Jun 2018, at 20:39, Richard Williamson <rwilli...@gmail.com<mailto:rwilli...@gmail.com>> wrote: Dear Thierry, Forgive me for not quite having an overview of exactly what has been done. My interest here is in how the model structure you have constructed compares with Cisinski's work. For example, I would expect that the category of cartesian cubical sets is a test category. Indeed, I would expect that more or less exactly the same technique as in 8.4 of Les préfaisceaux comme ... goes through to prove this. And I would expect that one can put a model structure on in the same way. Now, I believe I saw in some slides that that your model structure coincides with the Cisinski one. But this does not seem compatible with my expectations above, because then it is certainly Quillen equivalent to the Serre model structure on topological spaces (or whatever). Thus my questions: 1) Have I misinterpreted the slides or some other aspect of your work? 2) If not, where exactly do Cisinski's techniques fail? Best wishes, Richard [-- Attachment #2: Type: text/html, Size: 7455 bytes --] ^ permalink raw reply [flat|nested] 21+ messages in thread
* Re: [HoTT] Quillen model structure, PS 2018-06-14 18:39 ` Richard Williamson 2018-06-14 19:14 ` Steve Awodey 2018-06-14 19:16 ` Thierry Coquand @ 2018-06-14 19:35 ` Thierry Coquand 2 siblings, 0 replies; 21+ messages in thread From: Thierry Coquand @ 2018-06-14 19:35 UTC (permalink / raw) To: Richard Williamson; +Cc: Homotopy Theory I wrote —————— if we limit ourselves to the case where the base category is the Lawvere theory of distributive lattices, or de Morgan algebra, or Boolean algebra and we take the fibrations as defined page 13, we get the same notion as Cisinski -naive- fibrations. —————— I should have added that this is not completely trivial: it amounts to the fact that to have the -uniform- right lifting filling property w.r.t. any open box inclusion A x II \cup B x b -> B x II where B is -representable-, A -> B mono (where we have a choice of lifting that are natural w.r.t. map B’ -> B between representables) is -equivalent- to having the (non necessarily uniform) right lifting property w.r.t. -any- open box inclusion A x II \cup B x b -> B x II B arbitrary, A -> B mono The same holds (and is either to check) for trivial fibrations: to have the uniform right lifting property w.r.t. A -> B mono, B representable is equivalent to having the right lifting property w.r.t. an arbitrary mono. Best regards, Thierry > On 14 Jun 2018, at 20:39, Richard Williamson <rwilli...@gmail.com> wrote: > > Dear Thierry, > > Forgive me for not quite having an overview of exactly what has > been done. My interest here is in how the model structure you > have constructed compares with Cisinski's work. For example, I > would expect that the category of cartesian cubical sets is a > test category. Indeed, I would expect that more or less exactly > the same technique as in 8.4 of Les préfaisceaux comme ... goes > through to prove this. And I would expect that one can put a > model structure on in the same way. > > Now, I believe I saw in some slides that that your model > structure coincides with the Cisinski one. But this does not seem > compatible with my expectations above, because then it is > certainly Quillen equivalent to the Serre model structure on > topological spaces (or whatever). > > Thus my questions: > > 1) Have I misinterpreted the slides or some other aspect of your > work? > > 2) If not, where exactly do Cisinski's techniques fail? > > Best wishes, > Richard ^ permalink raw reply [flat|nested] 21+ messages in thread
end of thread, other threads:[~2018-06-14 21:07 UTC | newest] Thread overview: 21+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-06-10 13:31 Quillen model structure Thierry Coquand [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com> 2018-06-11 8:46 ` [HoTT] " Thierry Coquand 2018-06-13 20:33 ` Michael Shulman 2018-06-13 20:50 ` Steve Awodey 2018-06-13 22:00 ` Michael Shulman 2018-06-14 9:28 ` Steve Awodey 2018-06-14 9:48 ` Bas Spitters 2018-06-14 9:58 ` Christian Sattler 2018-06-14 10:27 ` Steve Awodey 2018-06-14 13:44 ` Steve Awodey 2018-06-14 14:52 ` Christian Sattler 2018-06-14 15:42 ` Steve Awodey 2018-06-14 15:47 ` Michael Shulman 2018-06-14 16:01 ` Steve Awodey 2018-06-14 18:39 ` Richard Williamson 2018-06-14 19:14 ` Steve Awodey 2018-06-14 20:15 ` Richard Williamson 2018-06-14 20:32 ` Ulrik Buchholtz 2018-06-14 21:07 ` Richard Williamson 2018-06-14 19:16 ` Thierry Coquand 2018-06-14 19:35 ` [HoTT] Quillen model structure, PS Thierry Coquand
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).