> > Exactly. It has been a little while since I was really working on > this stuff, so I could be forgetting something, but as far as I > know the test model structure on cartesian cubical sets is > exactly the one coming from the theorem of Cisinski that Thierry > cites using the obvious cylinder, and with empty S. Now, Thierry > also says, I believe, that this model structure is the same as > the one of Christian Sattler. How can this be?! > The weak equivalences of the test model structure form the least _regular_ test localizer. The identity adjunction gives a left Quillen functor from the type theoretic model structure to the test model structure, but this is only an equivalence when the weak equivalences of the former form a regular localizer (meaning: every presheaf is the homotopy colimit of its category of elements). BTW, for de Morgan (or Kleene) cubes, geometric realization is not even a left Quillen adjunct for the type theoretic model structure with all (decidable) monos as cofibrations, since the geometric realization of the inclusion of the union of the two diagonals into the square is not a topological cofibration (it's not even injective). There are “smaller” type theoretic model structures with fewer cofibrations, but even for those, geometric realization cannot be a Quillen equivalence. Best wishes, Ulrik