Další seminář z algebry se koná 27.5.2021 od 13.00 online na platformě ZOOM. Informace pro připojení a další program semináře je zde.

Raffael Stenzel

Proof relevance in higher topos theory

Abstrakt:
In the short course of its definition and early exploration, the theory of higher toposes (by which I specifically mean (infinity,1)-toposes) has been found to exhibit various traits which appear rather odd from the perspective of ordinary topos theory. Motivated by the fact that the internal language of every higher (Grothendieck) topos is a univalent type theory - and hence is intrinsically "proof relevant" - we reconsider the basic characteristic notions associated to a higher topos from a purely logical proof relevant point of view.
Given a small infinity-category C, this will motivate the notion of a  logical structure sheaf on C whose ideals correspond exactly to the left exact localizations of the infinity-category [C^{op},S] of presheaves over C. This in turn will naturally lead to a corresponding notion of generalized Grothendieck topologies on C which, first, capture all higher toposes embedded in [C^{op},S], and second, correspond exactly to the classical notion of Grothendieck topologies in the monic (i.e.\ the proof irrelevant) context. We will see that these notions induce a  Kripke-Joyal semantics valued in spaces (rather than in the classical subobject classifier) in obvious fashion as well. In the end of the talk we will take a look at a few examples of such topologies and, if time permits (which it rarely ever does, time appears to be pretty absolute when it comes to this), end with a discussion of some open questions.