From: Steve Awodey <awo...@cmu.edu>
To: Michael Shulman <shu...@sandiego.edu>
Cc: Thierry Coquand <Thierry...@cse.gu.se>,
Homotopy Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Quillen model structure
Date: Thu, 14 Jun 2018 11:28:04 +0200 [thread overview]
Message-ID: <DE1F3758-3F0D-4011-AE99-B713E1A228A8@cmu.edu> (raw)
In-Reply-To: <CAOvivQzMQLy243X_LSHFKzMtx5qRnzmt_Y+D-kwe-JqS9PFLTA@mail.gmail.com>
> On Jun 14, 2018, at 12:00 AM, Michael Shulman <shu...@sandiego.edu> wrote:
>
> In the 1-categorical case, I believe that every locally small
> (co)complete elementary 1-topos is defined over Set: its global
> sections functor has a left adjoint by cocompleteness, and the left
> adjoint is left exact by the Giraud exactness properties (which hold
> for any (co)complete elementary 1-topos). Such a topos can only fail
> to be Grothendieck by lacking a small generating set.
yes, that’s correct.
>
> In the oo-case, certainly cartesian cubical sets present a locally
> small (oo,1)-category (any model category does, at least assuming its
> locally small as a 1-category), so it seems to me there are three
> possibilities:
>
> 1. Although they are presumably an "elementary (oo,1)-topos" in the
> finitary sense that provides semantics for HoTT with HITs and
> univalent universes, they might fail to satisfy some of the oo-Giraud
> exactness properties. Presumably they are locally cartesian closed
> and coproducts are disjoint, so it would have to be that not all
> groupoids are effective.
that’s possible, I suppose …
>
> 2. They might lack a small generating set, i.e. the (oo,1)-category
> might not be locally presentable. Every combinatorial model category
> (i.e. cofibrantly generated model structure on a locally presentable
> 1-category) presents a locally presentable (oo,1)-category, and the
> 1-category of cartesian cubical sets is certainly locally presentable,
> but I suppose it's not obvious whether these weak factorization
> systems are cofibrantly generated.
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.
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.
>>
next prev parent reply other threads:[~2018-06-14 9:28 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 [this message]
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
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=DE1F3758-3F0D-4011-AE99-B713E1A228A8@cmu.edu \
--to="awo..."@cmu.edu \
--cc="Thierry..."@cse.gu.se \
--cc="homotopyt..."@googlegroups.com \
--cc="shu..."@sandiego.edu \
/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).