Re: [HoTT] Quillen model structure

[Michael Shulman <shu...@sandiego.edu>]

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.