Re: [HoTT] Quillen model structure

[Christian Sattler <sattler....@gmail.com>]

[-- 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 --]