From: Steve Awodey <awo...@cmu.edu>
To: Homotopy Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Quillen model structure
Date: Thu, 14 Jun 2018 17:42:13 +0200 [thread overview]
Message-ID: <C75D7A1E-4CFA-4B76-8239-A67D4CCC0DAA@cmu.edu> (raw)
In-Reply-To: <CALCpNBqnkiSkf4nRnQ6NyXUMABh0QdQMnN9BSXh2r1Sj-fjacA@mail.gmail.com>
[-- Attachment #1: Type: text/plain, Size: 9785 bytes --]
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 <awo...@cmu.edu <mailto:awo...@cmu.edu>> wrote:
>>
>>
>>
>>> On Jun 14, 2018, at 11:58 AM, Christian Sattler <sattler....@gmail.com <mailto:sattler....@gmail.com>> wrote:
>>>
>>> On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu <mailto: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 <mailto: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 <mailto: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 <mailto: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 <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 <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 <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> >>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> >>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>>> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
>
>
[-- Attachment #2: Type: text/html, Size: 20848 bytes --]
next prev parent reply other threads:[~2018-06-14 15:41 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-06-10 13:31 Thierry Coquand
[not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com>
2018-06-11 8:46 ` [HoTT] " Thierry Coquand
2018-06-13 20:33 ` Michael Shulman
2018-06-13 20:50 ` Steve Awodey
2018-06-13 22:00 ` Michael Shulman
2018-06-14 9:28 ` Steve Awodey
2018-06-14 9:48 ` Bas Spitters
2018-06-14 9:58 ` Christian Sattler
2018-06-14 10:27 ` Steve Awodey
2018-06-14 13:44 ` Steve Awodey
2018-06-14 14:52 ` Christian Sattler
2018-06-14 15:42 ` Steve Awodey [this message]
2018-06-14 15:47 ` Michael Shulman
2018-06-14 16:01 ` Steve Awodey
2018-06-14 18:39 ` Richard Williamson
2018-06-14 19:14 ` Steve Awodey
2018-06-14 20:15 ` Richard Williamson
2018-06-14 20:32 ` Ulrik Buchholtz
2018-06-14 21:07 ` Richard Williamson
2018-06-14 19:16 ` Thierry Coquand
2018-06-14 19:35 ` [HoTT] Quillen model structure, PS Thierry Coquand
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=C75D7A1E-4CFA-4B76-8239-A67D4CCC0DAA@cmu.edu \
--to="awo..."@cmu.edu \
--cc="homotopyt..."@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).