Re: [HoTT] Quillen model structure

[Steve Awodey <awo...@cmu.edu>]

> 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.