Re: [HoTT] Quillen model structure

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

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.