From: Thierry Coquand <Thierry...@cse.gu.se> To: "HomotopyT...@googlegroups.com" <HomotopyT...@googlegroups.com> 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, 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-toswitches of git-send-email(1): git send-email \ --in-reply-to=040A0397-9EFA-4503-BF91-CC1704526319@chalmers.se \ --to="thierry..."@cse.gu.se \ --cc="HomotopyT..."@googlegroups.com \ --subject='Re: constructive sheaf models' \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

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