Re: [HoTT] Quillen model structure

[Bas Spitters <b.a.w.s...@gmail.com>]

There has been some work by Nicolas Tabareau's group to try and prove
the exactness properties.
E.g.
https://homotopytypetheory.org/2016/01/08/colimits-in-hott/
https://jfr.unibo.it/article/download/6232/6389
and perhaps even later work.

It would be interesting if the Cartesian cubes would provide a
counterexample to this approach, and show that a 2-level type theory
is really needed.

On Thu, Jun 14, 2018 at 11:28 AM, Steve Awodey <awo...@cmu.edu> wrote:
>
>
>> 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.
>>>
>
> --
> 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.