Re: [HoTT] Quillen model structure

[Richard Williamson <rwilli...@gmail.com>]

> 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?!

I was mis-remembering. If one looks at 8.4.34 - 8.4.38 in Les
préfaisceaux ..., one sees that S is taken (of course, now that I
think properly about it!) to be the (non-empty!) set of horn
inclusions.

In summary, the difference, from the point of view of Cisinski's
theory, between the type-theoretic model structure and the test
model structure seems to be precisely the choice of S.

Thank you to all!