From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 14 Jun 2018 13:32:05 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <581216aa-9f1b-4f0c-8016-60532dadf61e@googlegroups.com> In-Reply-To: <20180614201503.GA1968@richard.richard> References: <20180614183959.GA1401@richard.richard> <54A8E26C-ECF8-441A-AC3F-7643DA47C3FE@cmu.edu> <20180614201503.GA1968@richard.richard> Subject: Re: [HoTT] Quillen model structure MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4103_1504518811.1529008325468" ------=_Part_4103_1504518811.1529008325468 Content-Type: multipart/alternative; boundary="----=_Part_4104_1060065398.1529008325469" ------=_Part_4104_1060065398.1529008325469 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > > Exactly. It has been a little while since I was really working on=20 > this stuff, so I could be forgetting something, but as far as I=20 > know the test model structure on cartesian cubical sets is=20 > exactly the one coming from the theorem of Cisinski that Thierry=20 > cites using the obvious cylinder, and with empty S. Now, Thierry=20 > also says, I believe, that this model structure is the same as=20 > the one of Christian Sattler. How can this be?!=20 > The weak equivalences of the test model structure form the least _regular_= =20 test localizer. The identity adjunction gives a left Quillen functor from the type=20 theoretic model structure to the test model structure, but this is only an= =20 equivalence when the weak equivalences of the former form a regular=20 localizer (meaning: every presheaf is the homotopy colimit of its category= =20 of elements). BTW, for de Morgan (or Kleene) cubes, geometric realization is not even a= =20 left Quillen adjunct for the type theoretic model structure with all=20 (decidable) monos as cofibrations, since the geometric realization of the= =20 inclusion of the union of the two diagonals into the square is not a=20 topological cofibration (it's not even injective). There are =E2=80=9Csmall= er=E2=80=9D type=20 theoretic model structures with fewer cofibrations, but even for those,=20 geometric realization cannot be a Quillen equivalence. Best wishes, Ulrik ------=_Part_4104_1060065398.1529008325469 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Exactly. It h= as 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 mode= l structure form the least _regular_ test localizer.

The identity adjunction gives a left Quillen functor from the type theor= etic model structure to the test model structure, but this is only an equiv= alence when the weak equivalences of the former form a regular localizer (m= eaning: 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 squ= are is not a topological cofibration (it's not even injective). There a= re =E2=80=9Csmaller=E2=80=9D type theoretic model structures with fewer cof= ibrations, but even for those, geometric realization cannot be a Quillen eq= uivalence.

Best wishes,
Ulrik
=
------=_Part_4104_1060065398.1529008325469-- ------=_Part_4103_1504518811.1529008325468--