Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
From: Thierry Coquand <Thierry...@cse.gu.se>
Subject: constructive sheaf models
Date: Fri, 17 Apr 2020 20:29:18 +0000	[thread overview]
Message-ID: <040A0397-9EFA-4503-BF91-CC1704526319@chalmers.se> (raw)

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

In the latest HoTTEST seminar

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Matthew Weaver made a reference to our work with Fabian Ruch on
constructive sheaf models. A link is

https://arxiv.org/abs/1912.10407

Here are some remarks (and an important correction) that may help in following
what we wrote and that will be incorporated in a future version:

-the analogy with morphisms of tribes (Section 1) is misleading.
We should have stated it instead as an analogy with the notion of morphisms
of -fibration category- (involving fibrations, equivalences, terminal objects and
pullbacks along fibrations).  We owe this correction to Christian Sattler.

-indeed what we use implicitly  in Section 1 is the notion of fibration category associated
to a type theory. This is described in particular in the work of Avigad-Kapulkin-Lumsdaine,
that we should have cited since it illuminates what is going on in the Appendix

-a lex operation D (figure 1 in the Appendix) is in particular a pointed endofunctor \eta_X : X -> DX
and we isolate in Section 1 two conditions for it to generate a lex modality

(1)  if \eta_X has a homotopy left inverse, it is an equivalence
(2)  D preserves etale fibration

(a fibration is etale if the corresponding diagram with the \eta maps is a homotopy pullback)

If MX, X -> MX is the homotopy initial D-algebra generated by X, then (1) implies that M defines a -modality-
(such that X is M-modal iff \eta_X is an equivalence)
and (1)+(2) imply that M is a -left exact modality- (the proof makes use of a universe)

-Definition 1.2 provides two sufficient conditions that imply respectively (1) and (2).
We check in Section 4 that these conditions hold for the “intuitive” notion of descent data
which is described in the introduction (and that Matthew described in his talk). If correct, this
provides a constructive description of the model of sheaf of spaces over a 1-site

-as mentioned by Matthew in his talk, the connections between this notion of descent data
and the cobar operation used by Mike Shulman in his recent work on strict univalent universes
need to be better understood

Best regards,
Thierry

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


                 reply	other threads:[~2020-04-17 20:29 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed


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,

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

switches of git-send-email(1):

git send-email \
--to="thierry..."@cse.gu.se \
--subject='Re: constructive sheaf models' \

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



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