open import Algebra.Prelude hiding (β«)

open import Cat.Functor.Equivalence.Complete
open import Cat.Instances.Sets.Cocomplete
open import Cat.Instances.Functor.Limits
open import Cat.Instances.Slice.Presheaf
open import Cat.Instances.Sets.Complete
open import Cat.Functor.Hom.Coyoneda
open import Cat.Functor.Equivalence
open import Cat.Diagram.Everything
open import Cat.Functor.Properties
open import Cat.Instances.Elements
open import Cat.Functor.Pullback
open import Cat.Instances.Slice
open import Cat.Instances.Lift
open import Cat.Functor.Slice

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 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 is a full subcategory of a presheaf category (the category is part of the definition) such that the inclusion functor 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 In particular, every universe generates a theory of the categories of sheaves on sites.

Fix a universe level and consider the category A topos might be a large category (i.e.Β it might have a space of objects with but it is essentially locally small, since it admits a fully-faithful functor into which have homs at level Hence, even if we allowed the category to have at a level we would have no more information there than fits in

For this reason, a topos only has two levels: The level of its objects, and the level of the category of Sets relative to which 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 consists of a set of points and a topology 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 is the poset 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 and family of subsets A lattice satisfying these properties (finite meets, arbitrary joins, the distributive law) is called a frame. A map of frames 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 which preserves finite meets and has a right adjoint 1.

We can prove that a topology on is the same thing as a subframe of its powerset β a collection of subsets of 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 is a sub-topos of a presheaf category We have essentially categorified βsubframeβ into βsubtoposβ, and into 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, 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 The objects of are then interpreted as βprimitive shapesβ, and the maps in are interpreted as βmaps to glue againstβ.

Letβs make this more concrete by considering an example: Take the category with two points β letβs call them and β and two arrows A presheaf on this category is given by a set a set and two functions We call the vertex set, and 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 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 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 enjoys many of the same categorical properties of the category (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 inherits the nice logical properties of (through the presheaf category, which is also very nice logically).

Terminology

As was implicitly mentioned above, for a topos we call the category the site of definition. Objects in are called sheaves, and the functor is called sheafification. Maps between topoi are called geometric morphisms, and will be defined below. We denote the 2-category of topoi, geometric morphisms and natural transformations by following Johnstone. When is regarded as a topos unto itself, rather than an indirection in the definition of a sheaf topos, we call it the topos of .

# Examplesπ

The βtrivialβ example of topoi is the category which is equivalently the category of presheaves on the terminal category. This is, in fact, the terminal object in the 2-category 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 is given by the βconstant presheafβ functor, which sends each set to the constant functor with value

  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 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 at its sole section and similarly by evaluating a natural transformation at its one component

  sets .L .Fβ F    = F # _
sets .L .Fβ nt   = nt # _
sets .L .F-id    = refl
sets .L .F-β f g = refl

These functors actually define an adjoint equivalence of categories, is continuous and, in particular, lex. Rather than appealing to that theorem, though, we define the preservation of finite limits directly for efficiency concerns.
  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
open _β£_
adj .unit = NT (Ξ» _ β idnt) Ξ» x y f β trivial!
adj .counit = NT (Ξ» _ β idnt) Ξ» x y f β trivial!


# Properties of topoiπ

The defining property of a topos is that it admits a geometric embedding into a presheaf category, meaning the adjunction is very special indeed: Since the right adjoint is fully faithful, the adjunction is monadic, meaning that it exhibits as the category of algebras for a (lex, idempotent) monad: the βsheafification monadβ. This gives us completeness in for βfreeβ (really, itβs because presheaf categories are complete, and those are complete because is.)

module _ {o ΞΊ} {π£ : Precategory o ΞΊ} (T : Topos ΞΊ π£) where
open Topos T

Sheafify : Monad (PSh ΞΊ site)

Topos-is-complete : is-complete ΞΊ ΞΊ π£
Topos-is-complete = equivalenceβcomplete
(Eilenberg-Moore-is-complete
(Functor-cat-is-complete (Sets-is-complete {ΞΉ = ΞΊ} {ΞΊ} {ΞΊ})))


Furthermore, since preserves colimits (it is a left adjoint), then we can compute the colimit of some diagram as the colimit (in of β which exists because is cocomplete β then apply to get a colimiting cocone for But the counit of the adjunction is a natural isomorphism, so we have a colimiting cocone for

  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 is an exponential ideal in If is a sheaf, and is any presheaf, then the internal hom is a sheaf: topoi are cartesian closed. Since topoi are defined as embedding faithfully into a category of presheaves, it follows that they have a small generating set, in the same sense that representables generate presheaves: In fact, the generating set of a Grothendieck topos is exactly the set of representables of its site! Elaborating, letting be a topos, two maps are equal if and only if they are equal under i.e.Β as maps of presheaves. But it follows from the coyoneda lemma that maps of presheaves are equal if and only if they are equal on all representables. Consequently, two maps in a are equal if and only if they agree on all generalised elements with domain the sheafification of a representable: module _ {o β} {C : Precategory o β} (ct : Topos β C) where private module C = Cat.Reasoning C module ct = Topos ct module Site = Cat.Reasoning (ct.site) module PSh = Cat.Reasoning (PSh β ct.site) module ΞΉ = Functor (ct.ΞΉ) module L = Functor (ct.L) open _β£_ (ct.Lβ£ΞΉ) open Functor open _=>_   Representables-generate : β {X Y} {f g : C.Hom X Y} β ( β {A} (h : C.Hom (L.β (γβ ct.site A)) X) β f C.β h β‘ g C.β h ) β f β‘ g Representables-generate {f = f} {g} sep = fully-faithfulβfaithful {F = ct.ΞΉ} ct.has-ff$
Representables-generate-presheaf ct.site Ξ» h β
ΞΉ.β f PSh.β h                                     β‘β¨ mangle β©β‘
ΞΉ.β β f C.β counit.Ξ΅ _ C.β L.β h β PSh.β unit.Ξ· _ β‘β¨ ap! (sep _) β©β‘
ΞΉ.β (g C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _   β‘Λβ¨ mangle β©β‘Λ
ΞΉ.β g PSh.β h                                     β

    where
mangle
: β {X Y} {f : C.Hom X Y} {Z} {h : PSh.Hom Z _}
β ΞΉ.β f PSh.β h β‘ ΞΉ.β (f C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _
mangle {f = f} {h = h} =
ΞΉ.β f PSh.β h                                                                  β‘β¨ PSh.insertl zag β©β‘
ΞΉ.β (counit.Ξ΅ _) PSh.β β unit.Ξ· _ PSh.β ΞΉ.β f PSh.β h β                        β‘β¨ ap! (PSh.extendl (unit.is-natural _ _ _)) β©β‘
ΞΉ.β (counit.Ξ΅ _) PSh.β ΞΉ.β (L.β (ΞΉ.β f)) PSh.β β unit.Ξ· _ PSh.β h β            β‘β¨ ap! (unit.is-natural _ _ _) β©β‘
ΞΉ.β (counit.Ξ΅ _) PSh.β β ΞΉ.β (L.β (ΞΉ.β f)) PSh.β ΞΉ.β (L.β h) PSh.β unit.Ξ· _ β  β‘β¨ ap! (PSh.pulll (sym (ΞΉ.F-β _ _))) β©β‘
ΞΉ.β (counit.Ξ΅ _) PSh.β ΞΉ.β (L.β (ΞΉ.β f) C.β L.β h) PSh.β unit.Ξ· _              β‘β¨ PSh.pulll (sym (ΞΉ.F-β _ _)) β©β‘
ΞΉ.β β counit.Ξ΅ _ C.β L.β (ΞΉ.β f) C.β L.β h β PSh.β unit.Ξ· _                    β‘β¨ ap! (C.extendl (counit.is-natural _ _ _)) β©β‘
ΞΉ.β (f C.β counit.Ξ΅ _ C.β L.β h) PSh.β unit.Ξ· _                                β


Finally, the property of βbeing a toposβ is invariant under slicing. More specifically, since a given topos can be presented by different sites, a presentation can be sliced under an object to present as a sheaf topos, with site of definition This follows from a wealth of pre-existing theorems:

• A pair of adjoint functors can be sliced under an object giving an adjunction Slicing a functor preserves full-faithfulness and left exactness, hence slicing a geometric embedding gives a geometric embedding.
• The category is equivalent to the category hence βbeing a presheaf topos is stable under slicingβ. Furthermore, this equivalence is part of an ambidextrous adjunction, hence both functors preserve limits.
• Dependent sum along an isomorphism is an equivalence of categories; But since a topos is presented by a reflective subcategory inclusion, the counit is an isomorphism.
module _ {o β} {C : Precategory o β} (T : Topos β C) (X : β C β) where
private
module C = Cat.Reasoning C
module Co = Cat.Reasoning (Slice C X)
module T = Topos T

open Topos
open Functor


We build the geometric embedding presenting as a topos by composing the adjunctions and β where is the equivalence The right adjoint is fully faithful because it composes two fully faithful functors (a slice of and an equivalence), the left adjoint preserves finite limits because it is a composite of two equivalences (hence two right adjoints) and a lex functor.

  Slice-topos : Topos β (Slice C X)
Slice-topos .site = β« T.site (T.ΞΉ.Fβ X)
Slice-topos .ΞΉ = sliceβtotal Fβ Sliced (T.ΞΉ) X
Slice-topos .has-ff = β-is-equiv (Sliced-ff {F = T.ΞΉ} (T.has-ff)) sliceβtotal-is-ff
Slice-topos .L = (Ξ£f (T .Lβ£ΞΉ.counit.Ξ΅ _) Fβ Sliced (T.L) (T.ΞΉ.Fβ X)) Fβ totalβslice

Slice-topos .L-lex =
Fβ-is-lex
(Fβ-is-lex
(is-equivalence.Fβ»ΒΉβ£F
(Ξ£-iso-equiv (C.isoβinvertible
(is-reflectiveβcounit-is-iso T.Lβ£ΞΉ T.has-ff)))))
(Sliced-lex T.L-lex))

Slice-topos .Lβ£ΞΉ = LFβ£GR (is-equivalence.Fβ»ΒΉβ£F sliceβtotal-is-equiv)


# Geometric morphismsπ

The definition of a topos as a generalisation of topological space leads us to look for a categorification of βcontinuous mapβ to functors between topoi. In the same way that a continuous function may be seen as a homomorphism of frames with defining feature the preservation of finite meets and arbitrary joins, we shall define a geometric morphism to be a functor which is left exact and admits a right adjoint.

Why the right adjoint? Well, right adjoints preserve limits, but by duality, left adjoints preserve colimits. This embodies the βarbitrary joinsβ part of a map of frames, whereas the βfinite meetsβ come from left exactness.

private
variable
o β o' β' ΞΊ ΞΊ' ΞΊ'' s s' : Level
E F G : Precategory o β
lvl : β {o β o' β'} β Precategory o β β Precategory o' β' β Level
lvl {o} {β} {o'} {β'} _ _ = o β β β β' β o'

record Geom[_,_] (E : Precategory o β) (F : Precategory o' β') : Type (lvl E F) where
no-eta-equality
field
Inv[_]  : Functor F E
Dir[_]  : Functor E F
Inv-lex : is-lex Inv[_]
Invβ£Dir : Inv[_] β£ Dir[_]

open Geom[_,_] public


Computation establishes that the identity functor is left exact, and self adjoint, so it is in particular both the direct and inverse image parts of a geometric morphism

Idg : Geom[ E , E ]
Idg {E = E} = record { Inv[_] = Id ; Dir[_] = Id
; Inv-lex = lex ; Invβ£Dir = adj }

  where
module E = Cat.Reasoning E

lex : is-lex Id
lex .is-lex.pres-β€ f = f
lex .is-lex.pres-pullback p = p

adj ._β£_.unit .Ξ· _ = E.id
adj ._β£_.unit .is-natural x y f = sym E.id-comm
adj ._β£_.counit .Ξ· _ = E.id
adj ._β£_.counit .is-natural x y f = sym E.id-comm


Since adjunctions compose, geometric morphisms do, too. Observe that the composite of inverse images and the composite of direct images go in different directions! Fortunately, this matches the convention for composing adjunctions, where the functors βswap sidesβ:

_Gβ_ : Geom[ F , G ] β Geom[ E , F ] β Geom[ E , G ]
f Gβ g = mk where
module f = Geom[_,_] f
module g = Geom[_,_] g
open is-lex

mk : Geom[ _ , _ ]
Inv[ mk ] = Inv[ g ] Fβ Inv[ f ]
Dir[ mk ] = Dir[ f ] Fβ Dir[ g ]
mk .Invβ£Dir = LFβ£GR f.Invβ£Dir g.Invβ£Dir


The composition of two left-exact functors is again left-exact, so thereβs no impediment to composition there, either.

  mk .Inv-lex .pres-β€ term ob = g.Inv-lex .pres-β€ (f.Inv-lex .pres-β€ term) _
mk .Inv-lex .pres-pullback pb = g.Inv-lex .pres-pullback (f.Inv-lex .pres-pullback pb)


An important class of geometric morphism is the geometric embedding, which weβve already met as the very definition of Topos. These are the geometric morphisms with fully faithful direct image. These are again closed under composition, so if we want to exhibit that a certain category is a topos, it suffices to give a geometric embedding where is some topos which is convenient for this application.

record Geom[_βͺ_] (E : Precategory o β) (F : Precategory o' β') : Type (lvl E F) where
field
morphism : Geom[ E , F ]
has-ff : is-fully-faithful Dir[ morphism ]

Geometric-embeddings-compose : Geom[ F βͺ G ] β Geom[ E βͺ F ] β Geom[ E βͺ G ]
Geometric-embeddings-compose f g =
record { morphism = f .morphism Gβ g .morphism
; has-ff = β-is-equiv (g .has-ff) (f .has-ff) }
where open Geom[_βͺ_]

Toposβgeometric-embedding : (T : Topos ΞΊ E) β Geom[ E βͺ PSh ΞΊ (T .Topos.site) ]
Toposβgeometric-embedding T = emb where
emb : Geom[ _ βͺ _ ]
Inv[ emb .Geom[_βͺ_].morphism ] = T .Topos.L
Dir[ emb .Geom[_βͺ_].morphism ] = T .Topos.ΞΉ
emb .Geom[_βͺ_].morphism .Inv-lex = T .Topos.L-lex
emb .Geom[_βͺ_].morphism .Invβ£Dir = T .Topos.Lβ£ΞΉ
emb .Geom[_βͺ_].has-ff = T .Topos.has-ff


1. By the adjoint functor theorem, any map between posets which preserves arbitrary joins has a right adjoint; Conversely, every map which has a right adjoint preserves arbitrary joins.β©οΈ