Re: [HoTT] Quillen model structure

[Steve Awodey <awo...@cmu.edu>]

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.