Understanding Higher Sites and Categorical Logic in Homotopy Type Theory 🧠

Homotopy Type Theory Electronic Seminar Talks, 2021-11-18
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

[In the following, read "higher'" as "(∞,1)-".]

It is a popular idiosyncrasy of higher toposes that, when defined in terms of Giraud-style axioms, a general representation result in terms of higher sheaf categories on a site appears to fail. Essentially, this discrepancy arises because "sites" here are implicitly understood to be higher categories equipped with proof-irrelevant (topo)logical data, while higher toposes are constructions within an intrinsically proof-relevant ambient world.

In the first part of the talk, we use this intuition of ambient proof-relevance to further develop the characterization of higher toposes over a given higher base topos in terms of their associated left exact modalities (Appendix of [1], and [2]). We give a definition of higher sites respective a small higher base category C which expresses "PreSh(C)-global localization" in terms of "C-indexed nullification" with respect to an associated sheaf of ideals. In this context I will also mention how one can derive an associated notion of higher Lawvere-Tierney topology as well (which is work in progress).

In the second part of the talk, we take a look at examples of such higher sites which are derived from classical examples considered in ordinary categorical logic. We will do so by simply ignoring the artificial propositional truncations implicit to these examples in the ordinary setting, and hence move away from the classical sheaf condition towards more general colimit-preserving properties. Such, so I hope, may be useful in the future for the study of the higher categorical semantics of intensional type theories.

[1] Rijke, Shulman, Spitters - Modalities in Homotopy Type Theory
[2] Anel, Biedermann, Finster, Joyal - Higher Sheaves