Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thierry Coquand <Thierry...@cse.gu.se>
To: Richard Williamson <rwilli...@gmail.com>
Cc: Homotopy Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Quillen model structure
Date: Thu, 14 Jun 2018 19:16:02 +0000	[thread overview]
Message-ID: <4B5790D8-1F4C-4964-86E5-4E77B07DD3BD@chalmers.se> (raw)
In-Reply-To: <20180614183959.GA1401@richard.richard>

[-- Attachment #1: Type: text/plain, Size: 4582 bytes --]


Dear Richard,

 The model structure is  not due to me but to Christian Sattler, and is explained in Section 2
of

 https://arxiv.org/pdf/1704.06911

(where I did some joint work is in the constructive argument that we have fibrant universes).

Cisinski defines in his book a model structure on presheaves where cofibrations
are monos. In order to define the model structure, one needs a “cylindre fonctoriel”
that we can define from a “segment”  II (a presheaf with two global distinct elements 0 and 1)
Exemple 1.3.8. We further need a “donnee homotopique”  Definition 1.3.14, given by a
set of monomorphism S. We only consider here the least case where S = empty set. From
this we can define a notion of anodyne map.
Given II and S, Cisinski explains then how to define a Quillen model structure Theorem 1.3.22
where

 -the cofibrations are the monomorphism
 -the anodyne maps are generated by open box inclusion, A x II \cup B x b -> B x II for A -> B
mono and b = 0,1
 -the fibrant objects are the ones having the extension property w.r.t. anodyne maps
 -the -naive- fibrations are the maps having the right lifting properties w.r.t. anodyne maps
(so a map X -> 1 is a naive fibration iff X if fibrant)
 -the weak equivalence are the maps A -> B such that for any fibrant X, the map
X^B -> X^A is a homotopy equivalence (w.r.t. the choice of the interval II)
 -the fibrations are the maps having the right lifting properties w.r.t. maps that are monos
and weak equivalence

 W.r.t. the slides at

http://uwo.ca/math/faculty/kapulkin/seminars/hottestfiles/Coquand-2018-05-24-HoTTEST.pdf

if we limit ourselves to the case where the base category is the Lawvere theory of
distributive lattices, or de Morgan algebra, or Boolean algebra and we take the fibrations
as defined page 13, we get the same notion as Cisinski -naive- fibrations.

 It follows from Section 2 of Christian’s paper above that we also get a model structure
having exactly this notion of fibration (and where cofibrations are monos).

 We then have a priori two model structures on these presheaves.
 They have the same notion
of fibrant objects and cofibrations. It follows then from André Joyal’s result
(Riehl Categorical Model Theory, Theorem 15.3.1) that we actually the -same- model
structure.

 It then follows that in these cases, the Cisinski model structure is -complete-
(Definition 1.3.48).

 In the case of de Morgan algebra, or distributive lattice, we have a geometric realisation map.
However in the case of de Morgan algebra, we don’t have that this map is a Quillen equivalence
as shown by Christian: if we take L to be the quotient of II by the de Morgan reversal operation
then the geometric realisation of L is contractible, but it can be shown that the map L -> 1
is not an equivalence for Cisinski (= Christian in this case) model structure.

 It is an open problem what happens for distributive lattices.

 I am not a specialist of test categories but my understanding is that all these categories
(Lawvere theory of distributive lattices, de Morgan algebra, algebra with two constants 0,1)
are test categories, but it is not clear if the general notion of weak equivalence we get
from the theory of test category coincide with the one of Cisinski model structure
(and indeed it will not coincide for de Morgan algebra and Boolean algebra, and this
is open for distributive lattices),

 Best regards,
 Thierry








On 14 Jun 2018, at 20:39, Richard Williamson <rwilli...@gmail.com<mailto:rwilli...@gmail.com>> wrote:

Dear Thierry,

Forgive me for not quite having an overview of exactly what has
been done. My interest here is in how the model structure you
have constructed compares with Cisinski's work. For example, I
would expect that the category of cartesian cubical sets is a
test category. Indeed, I would expect that more or less exactly
the same technique as in 8.4 of Les préfaisceaux comme ... goes
through to prove this. And I would expect that one can put a
model structure on in the same way.

Now, I believe I saw in some slides that that your model
structure coincides with the Cisinski one. But this does not seem
compatible with my expectations above, because then it is
certainly Quillen equivalent to the Serre model structure on
topological spaces (or whatever).

Thus my questions:

1) Have I misinterpreted the slides or some other aspect of your
work?

2) If not, where exactly do Cisinski's techniques fail?

Best wishes,
Richard


[-- Attachment #2: Type: text/html, Size: 7455 bytes --]

  parent reply	other threads:[~2018-06-14 19:16 UTC|newest]

Thread overview: 21+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-06-10 13:31 Thierry Coquand
     [not found] ` <CABLJ2vLi2ePKwf+Zha9Gx1jFgqJo9j2W0PsTctBZvf7F-xThHA@mail.gmail.com>
2018-06-11  8:46   ` [HoTT] " Thierry Coquand
2018-06-13 20:33 ` Michael Shulman
2018-06-13 20:50   ` Steve Awodey
2018-06-13 22:00     ` Michael Shulman
2018-06-14  9:28       ` Steve Awodey
2018-06-14  9:48         ` Bas Spitters
2018-06-14  9:58         ` Christian Sattler
2018-06-14 10:27           ` Steve Awodey
2018-06-14 13:44             ` Steve Awodey
2018-06-14 14:52               ` Christian Sattler
2018-06-14 15:42                 ` Steve Awodey
2018-06-14 15:47               ` Michael Shulman
2018-06-14 16:01                 ` Steve Awodey
2018-06-14 18:39 ` Richard Williamson
2018-06-14 19:14   ` Steve Awodey
2018-06-14 20:15     ` Richard Williamson
2018-06-14 20:32       ` Ulrik Buchholtz
2018-06-14 21:07       ` Richard Williamson
2018-06-14 19:16   ` Thierry Coquand [this message]
2018-06-14 19:35   ` [HoTT] Quillen model structure, PS Thierry Coquand

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=4B5790D8-1F4C-4964-86E5-4E77B07DD3BD@chalmers.se \
    --to="thierry..."@cse.gu.se \
    --cc="homotopyt..."@googlegroups.com \
    --cc="rwilli..."@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).