*constructive sheaf models@ 2020-04-17 20:29 Thierry Coquand0 siblings, 0 replies; only message in thread From: Thierry Coquand @ 2020-04-17 20:29 UTC (permalink / raw) To: HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] only message in thread

only message in thread, back to indexThread overview:(only message) (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2020-04-17 20:29 constructive sheaf models Thierry Coquand

Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Example config snippet for mirrors Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/public-inbox.git