Tag - Topos theory
In the short course of its definition and early exploration, the theory of higher toposes (by which I specifically mean (∞,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 ∞-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 [Cop, 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 [Cop, 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.
Comprehension schemes arose as crucial notions in the early work on the foundations of set theory, and hence they found expression in a considerable variety of foundational settings for mathematics. Particularly, they have been introduced to the context of categorical logic first by Lawvere and then by Benabou in the 1970s.
In this talk we define and study a theory of comprehension schemes for fibered ∞-categories, generalizing Johnstone’s respective notion for ordinary categories. This includes natural generalizations of all the fundamental instances originally defined by Benabou, and their application to Jacob's comprehension categories. Thereby, we can characterize
- numerous categorical structures arising in higher topos theory,
- the notion of univalence,
- internal ∞-categories,
in terms of comprehension schemes, while some of the 1-categorical counterparts fail to hold in ordinary category theory. As an application, we can show that the universal cartesian fibration is represented via externalization by the "freely walking chain" in the ∞-category of small ∞-categories.
In the end, if my time management permits, we take a look at the externalization construction of internal ∞-categories from a model categorical perspective and review some examples from the literature in this light.
We introduce structures called globular multicategories with homomorphism types. We discuss how various collections of "higher category-like" objects can be used to to construct these globular multicategories. We show how to obtain a number of higher categorical structures using this data. We will see that in this setting there is a precise sense in which:
- types are higher categories,
- dependent types are profunctors,
- terms are higher functors,
- terms in a dependent context are higher transformations,
- there is a higher category of all types and terms.
Many prominent dualities in mathematics are instances of a common construction centered on the notion of spectral functor. Roughly stated, one starts with a locally finitely presentable category, equipped with a subcategory of distinguished local objects encoding point-like data and a factorization system (Étale maps, Local maps) where the etale maps behave as duals of distinguished continuous maps. Several manners of axiomatizing the correct relation between those ingredients have been proposed, either through topos theoretic methods by "localizing" local objects with a Grothendieck topology generated by étale maps, or in an alternative (though tightly related) way based on the notion of local right ajoint (or equivalently stable functor). Then the spectrum of a given object is constructed as a topos classifying etale maps under this given object toward local objects, equipped with a structural sheaf playing the role of the "free local object" under it. This defines a spectral functor from the ambient locally finitely presentable category to a category of locally structured toposes, forming an adjunction with a corresponding global section functor. This construction provide a convenient template for several prominent 1-categorical examples, as dualities for rings in algebraic geometry, or also Stone-like dualities for different classes of propositional algebras. The strong analogy between those dualities and their corresponding first order syntax-semantics dualities suggests the later could be understood as instances of a convenient 2-dimensional spectral construction. In this talk we will expose the ongoing work devoted to concretize this intuition.
After recalling the 1-dimensional version of the construction and the details of some prominent Stone-like examples, we introduces a notion of stable 2-functor and provide a method to construct an associated notion of spectral 2-sites, defining the spectrum as the associated Grothendieck 2-topos equipped with a distinguished structural stack. In particular we give a special interest in determining the local objects and the factorization system associated to doctrines corresponding to fragments of first order logics, as Lex, Reg, or Coh; in those situations, the construction simplifies as the spectral site happens to be 1-truncated so that one recover the corresponding 1-dimensional notion of classifying topos of a theory as the spectrum, and the geometry of the spectrum actually arises from the geometric properties of local toposes and étale geometric morphisms.
In this talk we will delve into the background details of the previous talk by introducing syntactic proof systems and their categorical semantics, including the construction of syntactic categories and κ-classifying toposes, as well as the role of certain properties of Grothendieck topologies and
Kripke-Joyal semantics. We will then study some topos-theoretic completeness theorems for certain infinitary logics that generalize results of Deligne and Joyal.
You must be logged in to post a comment.