Re: [HoTT] Quillen model structure

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

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.

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.

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.

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