On Thu, Jun 14, 2018 at 3:44 PM, Steve Awodey 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 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 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 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 >> 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 >> >>> 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. > > >