open import Cat.CartesianClosed.Instances.PSh
open import Cat.Diagram.Everything
open import Cat.Functor.Properties
open import Cat.Instances.Functor
open import Cat.Prelude

open import Topoi.Base

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

module Topoi.Reasoning where


# Reasoning in topoiπ

As mentioned in the overture on topos theory, categories of sheaves are incredibly nice categories to work in logically, mirroring many of the same properties of the category of Sets. This follows from the fact that they are reflective subcategories of presheaf categories, and those categories enjoy many of the exactness properties of $\mathbf{Sets}$ by virtue of being functor categories.

This module provides a companion to the overture which makes it more convenient to reason about a particular sheaf topos by computing explicit descriptions of finite limits and colimits, and establishing the key exactness properties of a topos: Coproducts are disjoint, equivalence relations are effective, and colimits are stable under pullback.

module Sheaf-topos {o β} {π― : Precategory o β} (T : Topos β π―) where
open Cat π― public
open _β£_ (T .Topos.Lβ£ΞΉ) public

module L = Func (T .Topos.L)
module L-lex = is-lex (T .Topos.L-lex)
module ΞΉ = Func (T .Topos.ΞΉ)

open Topos T using (site) public

module Presh = Cat (PSh β site)

LΞΉ-iso : β x β is-invertible (counit.Ξ΅ x)
LΞΉ-iso x = isoβinvertible
(is-reflectiveβcounit-is-iso (T .Topos.Lβ£ΞΉ) (T .Topos.has-ff))

Ξ΅β»ΒΉ : Id => T .Topos.L Fβ T .Topos.ΞΉ
Ξ΅β»ΒΉ = Cat._β_.from (is-reflectiveβcounit-iso (T .Topos.Lβ£ΞΉ) (T .Topos.has-ff))
module Ξ΅β»ΒΉ = _=>_ Ξ΅β»ΒΉ

psh-equal : β {X Y} {f g : Hom X Y} β ΞΉ.β f β‘ ΞΉ.β g β f β‘ g
psh-equal = fully-faithfulβfaithful {F = T .Topos.ΞΉ} (T .Topos.has-ff)

Terminology

We will refer to the objects of $\mathcal{C}$, the topos, as sheaves, and the objects of $[S^{\mathrm{op}},\mathbf{Sets}]$ as presheaves. Correspondingly, the left adjoint functor $[S^{\mathrm{op}}, \mathbf{Sets}] \to \mathcal{C}$ is called sheafification.

## Limitsπ

Since the sheafification functor is left exact and the inclusion functor is fully faithful (thus the adjunction counit is an isomorphism, c.f. LΞΉ-iso), we can compute limits directly in the presheaf category and sheafify. Unfolding the result of this procedure, rather than appealing to the equivalence $\mathcal{C} \cong [S^{\mathrm{op}},\mathbf{Sets}]^{L\iota}$, yields much better computational properties. We do it by hand for the terminal object, binary products, and binary pullbacks.

  open Terminal
terminal-sheaf : Terminal π―
terminal-sheaf .top = L.β (PSh-terminal {C = site} .top)
terminal-sheaf .hasβ€ = L-lex.pres-β€ (PSh-terminal {C = site} .hasβ€)

product-sheaf : β A B β Product π― A B
product-sheaf A B = productβ² where
product-presheaf : Product (PSh β site) (ΞΉ.β A) (ΞΉ.β B)
product-presheaf = PSh-products {C = site} _ _

open Product
productβ² : Product π― A B
productβ² .apex = L.β (product-presheaf .apex)
productβ² .Οβ = counit.Ξ΅ _ β L.β (product-presheaf .Οβ)
productβ² .Οβ = counit.Ξ΅ _ β L.β (product-presheaf .Οβ)
productβ² .has-is-product =
let
prod =
L-lex.pres-product
(PSh-terminal {C = site} .hasβ€)
(product-presheaf .has-is-product)
in is-product-iso π― (LΞΉ-iso _) (LΞΉ-iso _) prod

open Binary-products π― product-sheaf public


The computation for finite connected limits (pullbacks, equalisers) is a bit more involved, but not by much:

  pullback-sheaf
: β {X Y Z} (f : Hom X Z) (g : Hom Y Z)
β Pullback π― f g
pullback-sheaf f g = pullbackβ² where
pullback-presheaf : Pullback (PSh β site) (ΞΉ.β f) (ΞΉ.β g)
pullback-presheaf = PSh-pullbacks {C = site} _ _

open Pullback
open is-pullback
module Pb = Pullback pullback-presheaf
module lpb = is-pullback (L-lex.pres-pullback (pullback-presheaf .has-is-pb))

pullbackβ² : Pullback π― f g
pullbackβ² .apex = L.β Pb.apex
pullbackβ² .pβ = counit.Ξ΅ _ β L.β Pb.pβ
pullbackβ² .pβ = counit.Ξ΅ _ β L.β Pb.pβ
pullbackβ² .has-is-pb = pbβ² where
pbβ² : is-pullback π― _ f _ g
pbβ² .square = squareβ² where abstract
squareβ² : f β counit.Ξ΅ _ β L.β Pb.pβ β‘ g β counit.Ξ΅ _ β L.β Pb.pβ
squareβ² =
f β counit.Ξ΅ _ β L.β Pb.pβ           β‘β¨ extendl (sym (counit.is-natural _ _ _)) β©β‘
counit.Ξ΅ _ β L.β (ΞΉ.β f) β L.β Pb.pβ β‘β¨ reflβ©ββ¨ lpb.square β©β‘
counit.Ξ΅ _ β L.β (ΞΉ.β g) β L.β Pb.pβ β‘β¨ extendl (counit.is-natural _ _ _) β©β‘
g β counit.Ξ΅ _ β L.β Pb.pβ           β

pbβ² .universal {pβ' = pβ'} {pβ'} p =
lpb.universal {pβ' = Ξ΅β»ΒΉ.Ξ· _ β pβ'} {pβ' = Ξ΅β»ΒΉ.Ξ· _ β pβ'} path
where abstract
path : L.β (ΞΉ.β f) β Ξ΅β»ΒΉ.Ξ· _ β pβ' β‘ L.β (ΞΉ.β g) β Ξ΅β»ΒΉ.Ξ· _ β pβ'
path =
L.β (ΞΉ.β f) β Ξ΅β»ΒΉ.Ξ· _ β pβ' β‘β¨ extendl (sym (Ξ΅β»ΒΉ.is-natural _ _ _)) β©β‘
Ξ΅β»ΒΉ.Ξ· _ β g β pβ'           β‘β¨ extendl (Ξ΅β»ΒΉ.is-natural _ _ _) β©β‘
L.β (ΞΉ.β g) β Ξ΅β»ΒΉ.Ξ· _ β pβ' β

pbβ² .pββuniversal =
pullr lpb.pββuniversal β cancell (LΞΉ-iso _ .is-invertible.invl)
pbβ² .pββuniversal =
pullr lpb.pββuniversal β cancell (LΞΉ-iso _ .is-invertible.invl)
pbβ² .unique p q = lpb.unique
(sym ( apβ _β_ refl (sym p β sym (assoc _ _ _))
β cancell (LΞΉ-iso _ .is-invertible.invr)))
(sym ( apβ _β_ refl (sym q β sym (assoc _ _ _))
β cancell (LΞΉ-iso _ .is-invertible.invr)))

finitely-complete : Finitely-complete π―
finitely-complete .Finitely-complete.terminal = terminal-sheaf
finitely-complete .Finitely-complete.products = product-sheaf
finitely-complete .Finitely-complete.equalisers =
with-pullbacks π― terminal-sheaf pullback-sheaf
.Finitely-complete.equalisers
finitely-complete .Finitely-complete.pullbacks = pullback-sheaf