open import Cat.Functor.Equivalence.Complete
open import Cat.Functor.Adjoint.Continuous
open import Cat.Functor.Adjoint.Reflective
open import Cat.Instances.Algebras.Limits
open import Cat.Instances.Sets.Cocomplete
open import Cat.Instances.Functor.Limits
open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Slice.Presheaf
open import Cat.Functor.Adjoint.Compose
open import Cat.Functor.Adjoint.Monadic
open import Cat.Instances.Sets.Complete
open import Cat.Functor.Adjoint.Monad
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Finite
open import Cat.Functor.Hom.Coyoneda
open import Cat.Functor.Equivalence
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Properties
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Diagram.Pullback
open import Cat.Functor.Pullback
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Instances.Lift
open import Cat.Diagram.Monad
open import Cat.Functor.Slice
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor
import Cat.Reasoning

module Topoi.Base where

open _=>_

Grothendieck topoi🔗

Topoi are an abstraction introduced by Alexander Grothendieck in the 1960s as a generalisation of topological spaces, suitable for his work in algebraic geometry. Later (in the work of William Lawvere, and even later Myles Tierney), topoi found a new life as “categories with a nice internal logic”, which mirrors that of the category $\mathbf{Sets}\text{.}$ Perhaps surprisingly, every Grothendieck topos is also a topos in their logical conception (called elementary); Since elementary topoi are very hard to come by predicatively, we formalise a particular incarnation of Grothendieck’s notion here.

Grothendieck described his topoi by first defining a notion of site, which generalises the (poset of) open subsets of a topological space, and then describing what “sheaves on a site” should be, the corresponding generalisation of sheaves on a space. Instead of directly defining the notion of site, we will leave it implicitly, and define a topos as follows:

A topos $\mathcal{T}$ is a full subcategory of a presheaf category $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]$ (the category $\mathcal{C}$ is part of the definition) such that the inclusion functor $\iota :\mathcal{T}\hookrightarrow [{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]$ admits a left adjoint, and this left adjoint preserves finite limits. We summarise this situation in the diagram below, where “lex” (standing for “left exact”) is old-timey speak for “finite limit preserving”.

In type theory, we must take care about the specific universes in which everything lives. Now, much of Grothendieck topos theory generalises to arbitrary “base” topoi, via the use of bounded geometric morphisms, but the “main” definition talks about $\mathbf{Sets}\text{-topoi.}$ In particular, every universe $\kappa$ generates a theory of ${\mathbf{Sets}}_{\kappa }\text{-topoi,}$ the categories of $\kappa \text{-small}$ sheaves on $\kappa \text{-small}$ sites.

Fix a universe level $\kappa \text{,}$ and consider the category ${\mathbf{Sets}}_{\kappa }\text{:}$ A topos $\mathcal{T}$ might be a large category (i.e. it might have a space of objects $o$ with $o>\kappa \text{),}$ but it is essentially locally small, since it admits a fully-faithful functor into $[{\mathcal{C}}^{\mathrm{op}},{\mathbf{Sets}}_{\kappa }]\text{,}$ which have homs at level $\kappa \text{.}$ Hence, even if we allowed the category $\mathcal{T}$ to have $\mathbf{Hom}\text{s}$ at a level $\ell \text{,}$ we would have no more information there than fits in $\kappa \text{.}$

For this reason, a topos $\mathcal{C}$ only has two levels: The level $o$ of its objects, and the level $\kappa$ of the category of Sets relative to which $\mathcal{C}$ is a topos.

record Topos {o} κ (𝓣 : Precategory o κ) : Type (lsuc (o ⊔ κ)) where
  field
    site : Precategory κ κ

    ι : Functor 𝓣 (PSh κ site)
    has-ff : is-fully-faithful ι

    L : Functor (PSh κ site) 𝓣
    L-lex : is-lex L

    L⊣ι : L ⊣ ι

  module ι = Functor ι
  module L = Functor L
  module L⊣ι = _⊣_ L⊣ι

As generalised spaces🔗

I’ll echo here the standard definition of topological space, but due to personal failings I can’t motivate it. A topological space $(X,\tau )$ consists of a set of points $X\text{,}$ and a topology $\tau \text{,}$ a subset of its powerset which is closed under arbitrary unions and finite intersections.

Let’s reword that using category-theoretic language: Recall that the powerset of $X$ is the poset $[X,\mathbf{Props}]\text{.}$ It is — being a functor category into a complete and cocomplete (thin) category — also complete and cocomplete, so all joins and finite meets (unions and intersections) exist; Furthermore, the distributive law

holds for any subset $S$ and family of subsets $F\text{.}$ A lattice satisfying these properties (finite meets, arbitrary joins, the distributive law) is called a frame. A map of frames $f:A\to B$ is defined to be a map of their underlying sets preserving finite meets and arbitrary joins — by abstract nonsense, this is the same as a function $f^{\ast }:A\to B$ which preserves finite meets and has a right adjoint $f_{\ast }:B\to A$¹.

We can prove that a topology $\tau$ on $X$ is the same thing as a subframe of its powerset $[X,\mathbf{Props}]$ — a collection of subsets of $X\text{,}$ closed under finite meets and arbitrary joins.

Now, the notion of “topos” as a generalisation of that of “topological space” is essentially self-evident: A topos $\mathcal{T}$ is a sub-topos of a presheaf category $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]\text{.}$ We have essentially categorified “subframe” into “subtopos”, and $\mathbf{Props}$ into $\mathbf{Sets}\text{.}$ Note that, while this seems circular (“a topos is a sub-topos of…”), the notion of subtopos — or rather, of geometric embedding — makes no mention of actual topoi, and makes sense for any pair of categories.

As categories of spaces🔗

Another perspective on topoi is that they are categories of spaces, rather than spaces themselves. We start by looking at presheaf topoi, $[{\mathcal{C}}^{\mathrm{op}},\mathbf{Sets}]\text{.}$ The coyoneda lemma tells us that every presheaf is a colimit of representables, which can be restated in less abstract terms by saying that presheaves are instructions for gluing together objects of $\mathcal{C}\text{.}$ The objects of $\mathcal{C}$ are then interpreted as “primitive shapes”, and the maps in $\mathcal{C}$ are interpreted as “maps to glue against”.

Let’s make this more concrete by considering an example: Take $\mathcal{C}=\bullet \rightrightarrows \bullet \text{,}$ the category with two points — let’s call them $V$ and $E$ — and two arrows $s,t:V\to E\text{.}$ A presheaf $F$ on this category is given by a set $F_0(V)\text{,}$ a set $F_0(E)\text{,}$ and two functions $F_1(s),F_1(t):F_0(E)\to F_0(V)\text{.}$ We call $F_0(V)$ the vertex set, and $F_0(E)$ the edge set. Indeed, a presheaf on this category is a directed multigraph, and maps between presheaves preserve adjacency.

Our statement about “gluing primitive shapes” now becomes the rather pedestrian statement “graphs are made up of vertices and edges”. For instance, the graph $\bullet \to \bullet \to \bullet$ can be considered as a disjoint union of two edges, which is then glued together in a way such that the target of the first is the source of the second. The maps $s,t:V\to E$ exhibit the two ways that a vertex can be considered “part of” an edge.

As “logically nice” categories🔗

The definition of topos implies that any topos $\mathcal{T}$ enjoys many of the same categorical properties of the category $\mathbf{Sets}$ (see below). Topoi are complete and cocomplete, cartesian closed (even locally so) — colimits are stable under pullback, coproducts are disjoint, and equivalence relations are effective.

These properties, but especially local cartesian closure, imply that the internal logic of a topos is an incredibly nice form of type theory. Dependent sums and products exist, there is an object of natural numbers, the poset of subobjects of any object is a complete lattice (even a Heyting algebra), including existential and universal quantification. Effectivity of congruences means that two points in a quotient are identified if, and only if, they are related by the congruence.

In fact, this is essentially the definition of a topos. The actual definition, as a lex reflective subcategory of a presheaf category, essentially ensures that the category $\mathcal{T}$ inherits the nice logical properties of $\mathbf{Sets}$ (through the presheaf category, which is also very nice logically).

Examples🔗

The “trivial” example of topoi is the category $\mathbf{Sets}\text{,}$ which is equivalently the category $[{\ast }^{\mathrm{op}},\mathbf{Sets}]$ of presheaves on the terminal category. This is, in fact, the terminal object in the 2-category $\mathfrak{Topos}$ of topoi (morphisms are described below), so we denote it by 𝟙.

𝟙 : ∀ {κ} → Topos κ (Sets κ)
𝟙 {κ} = sets where
  open Topos
  open Functor
  open _⊣_
  open is-lex

The inclusion functor $\mathbf{Sets}\hookrightarrow \mathrm{PSh}(\ast )$ is given by the “constant presheaf” functor, which sends each set $X$ to the constant functor with value $X\text{.}$

  incl : Functor (Sets κ) (PSh κ (Lift-cat κ κ ⊤Cat))
  incl .F₀ x .F₀ _    = x
  incl .F₀ x .F₁ _ f  = f
  incl .F₀ x .F-id    = refl
  incl .F₀ x .F-∘ f g = refl

  incl .F₁ f = NT (λ _ → f) (λ _ _ _ → refl)

  incl .F-id    = trivial!
  incl .F-∘ f g = trivial!

  sets : Topos κ (Sets κ)
  sets .site = Lift-cat κ κ ⊤Cat

  sets .ι = incl

This functor is fully faithful since a natural transformation between presheaves on the point is entirely determined by its component at.. well, the point. Hence, the map $\eta \mapsto {\eta }_{\ast }$ exhibits an inverse to the inclusion functor’s action on morphisms, which is sufficient (and necessary) to conclude fully-faithfulness.

  sets .has-ff {x} {y} = is-iso→is-equiv isic where
    open is-iso
    isic : is-iso (incl .F₁ {x} {y})
    isic .inv  nt = nt .η _
    isic .rinv nt = trivial!
    isic .linv f  = refl

The “sheafification” left adjoint is given by evaluating a presheaf $F$ at its sole section $F(\ast )\text{,}$ and similarly by evaluating a natural transformation $\eta :F\Rightarrow G$ at its one component ${\eta }_{\ast }:F(\ast )\to G(\ast )\text{.}$

  sets .L .F₀ F    = F · _
  sets .L .F₁ nt   = nt · _
  sets .L .F-id    = refl
  sets .L .F-∘ f g = refl

  sets .L-lex .pres-⊤ {T} psh-terminal set = contr (cent .η _) uniq where
    func = incl .F₀ set
    cent = psh-terminal func .centre
    uniq : ∀ f → cent .η _ ≡ f
    uniq f = psh-terminal func .paths f' ηₚ _ where
      f' : _ => _
      f' .η _ = f
      f' .is-natural _ _ _ = funext λ x → happly (sym (T .F-id)) _

  sets .L-lex .pres-pullback {P} {X} {Y} {Z} pb = pb' where
    open is-pullback
    pb' : is-pullback (Sets κ) _ _ _ _
    pb' .square = pb .square ηₚ _
    pb' .universal {P'} {p₁' = p₁'} {p₂' = p₂'} p =
      pb .universal {P' = incl · P'}
        {p₁' = NT (λ _ → p₁') (λ _ _ _ → funext λ _ → sym (X .F-id · _))}
        {p₂' = NT (λ _ → p₂') (λ _ _ _ → funext λ _ → sym (Y .F-id · _))}
        (Nat-pathp _ _ (λ x → p)) · lift tt

    pb' .p₁∘universal = pb .p₁∘universal ηₚ _
    pb' .p₂∘universal = pb .p₂∘universal ηₚ _
    pb' .unique {P'} {lim' = lim'} p1 p2 =
      pb .unique {lim' = l'} (Nat-pathp _ _ λ _ → p1) (Nat-pathp _ _ λ _ → p2) ηₚ _
      where
        l' : incl .F₀ P' => P
        l' .η _ = lim'
        l' .is-natural x y f i o = P .F-id (~ i) (lim' o)

Similarly, we can construct the adjunction unit and counit by looking at components and constructing identity natural transformations.

  sets .L⊣ι .unit .η _ .η _ f            = f
  sets .L⊣ι .unit .η F .is-natural _ _ _ = F .F-id
  sets .L⊣ι .unit .is-natural _ _ _      = trivial!

  sets .L⊣ι .counit .η _ x            = x
  sets .L⊣ι .counit .is-natural _ _ _ = refl

  sets .L⊣ι .zig = refl
  sets .L⊣ι .zag = trivial!

More canonical examples are given by any presheaf category, where both the inclusion and sheafification functors are the identity. Examples of presheaf topoi are abundant in abstract homotopy theory (the categories of cubical and simplicial sets) — which also play an important role in modelling homotopy type theory; Another example of a presheaf topos is the category of quivers (directed multigraphs).

Presheaf : ∀ {κ} (C : Precategory κ κ) → Topos κ (PSh κ C)
Presheaf {κ} C = psh where
  open Functor
  open Topos
  psh : Topos _ _
  psh .site = C
  psh .ι = Id
  psh .has-ff = id-equiv
  psh .L = Id
  psh .L-lex .is-lex.pres-⊤ c = c
  psh .L-lex .is-lex.pres-pullback pb = pb
  psh .L⊣ι = adj where
    open _⊣_
    adj : Id ⊣ Id
    adj .unit = NT (λ _ → idnt) λ x y f → trivial!
    adj .counit = NT (λ _ → idnt) λ x y f → trivial!
    adj .zig = trivial!
    adj .zag = trivial!

Properties of topoi🔗

The defining property of a topos $\mathcal{T}$ is that it admits a geometric embedding into a presheaf category, meaning the adjunction $L:\mathcal{T}\rightleftarrows \mathrm{PSh}(\mathcal{C}):\iota$ is very special indeed: Since the right adjoint is fully faithful, the adjunction is monadic, meaning that it exhibits $\mathcal{T}$ as the category of algebras for a (lex, idempotent) monad: the “sheafification monad”. This gives us completeness in $\mathcal{T}$ for “free” (really, it’s because presheaf categories are complete, and those are complete because $\mathbf{Sets}$ is.)

module _ {o κ} {𝓣 : Precategory o κ} (T : Topos κ 𝓣) where
  open Topos T

  Sheafify : Monad-on _
  Sheafify = Adjunction→Monad L⊣ι

  Sheafify-monadic : is-monadic L⊣ι
  Sheafify-monadic = is-reflective→is-monadic L⊣ι has-ff

  Topos-is-complete : is-complete κ κ 𝓣
  Topos-is-complete = equivalence→complete
    (is-equivalence.inverse-equivalence Sheafify-monadic)
    (Eilenberg-Moore-is-complete _
      (Functor-cat-is-complete (Sets-is-complete {ι = κ} {κ} {κ})))

Furthermore, since $L$ preserves colimits (it is a left adjoint), then we can compute the colimit of some diagram $F:J\to \mathcal{T}$ as the colimit (in $\mathrm{PSh}(\mathcal{C})\text{)}$ of $\iota F$ — which exists because $\mathbf{Sets}$ is cocomplete — then apply $L$ to get a colimiting cocone for $L\iota F\text{.}$ But the counit of the adjunction $\epsilon :L\iota \Rightarrow \mathrm{Id}$ is a natural isomorphism, so we have a colimiting cocone for $F\text{.}$

  Topos-is-cocomplete : is-cocomplete κ κ 𝓣
  Topos-is-cocomplete F =
    natural-iso→colimit
      (F∘-iso-id-l (is-reflective→counit-iso L⊣ι has-ff))
      sheafified
      where
      psh-colim : Colimit (ι F∘ F)
      psh-colim = Functor-cat-is-cocomplete (Sets-is-cocomplete {ι = κ} {κ} {κ}) _

      sheafified : Colimit ((L F∘ ι) F∘ F)
      sheafified = subst Colimit F∘-assoc $
        left-adjoint-colimit L⊣ι psh-colim

Since the reflector is left exact, and thus in particular preserves finite products, a theorem of Johnstone (Elephant A4.3.1) implies the topos $\mathcal{T}$ is an exponential ideal in $\mathrm{PSh}(\mathcal{C})\text{:}$ If $Y$ is a sheaf, and $X$ is any presheaf, then the internal hom $[X,Y]$ is a sheaf: topoi are cartesian closed.