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 > wrote: >> >> >> >>> On Jun 14, 2018, at 11:58 AM, Christian Sattler > 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 . > >