Re: [HoTT] Quillen model structure

[Ulrik Buchholtz <ulrikbu...@gmail.com>]

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


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


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