Hello Sorry for this problem. I should have used the following link https://ncatlab.org/homotopytypetheory/files/awodeyMURI18.pdf Best regards, Thierry On 11 Jun 2018, at 10:28, Hiroyuki Miyoshi > wrote: Hi, Thierry, Your note is very interesting for me! Unfortunately, the Awodey's filie you mentioned in your message seems to be (still?) private and I cannot read it: https://ncatlab.org/hottmuri/files/awodeyMURI18.pdf If you (or Steve?) can change the status of the file, please make it public. Thanks in advance. Hiroyuki Miyoshi, Dept of Mathematics, Kyoto Sangyo University, Kyoto, Japan h...@cc.kyoto-su.ac.jp 2018年6月10日(日) 22:31 Thierry Coquand >: 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.