Quillen model structure

[Thierry Coquand <Thierry...@cse.gu.se>]

[-- Attachment #1.1: Type: text/plain, Size: 2768 bytes --]

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.


[-- Attachment #1.2: Type: text/html, Size: 4870 bytes --]

[-- Attachment #2: fact1.pdf --]
[-- Type: application/pdf, Size: 168794 bytes --]