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.