open import Cat.CartesianClosed.Instances.PSh
open import Cat.Diagram.Everything
open import Cat.Functor.Everything
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 $\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\op,\sets]$ as presheaves. Correspondingly, the left adjoint functor $[S\op, \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\op,\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 Cartesian 𝒯 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′ .limiting {p₁' = p₁'} {p₂'} p =
lpb.limiting {p₁' = ε⁻¹.η _ ∘ p₁'} {p₂' = ε⁻¹.η _ ∘ p₂'} path
where abstract
path : L.₁ (ι.₁ f) ∘ ε⁻¹.η _ ∘ p₁' ≡ L.₁ (ι.₁ g) ∘ ε⁻¹.η _ ∘ p₂'
path =
L.₁ (ι.₁ f) ∘ ε⁻¹.η _ ∘ p₁' ≡⟨ extendl (sym (ε⁻¹.is-natural _ _ _)) ⟩≡
ε⁻¹.η _ ∘ f ∘ p₁'           ≡⟨ refl⟩∘⟨ p ⟩≡
ε⁻¹.η _ ∘ g ∘ p₂'           ≡⟨ extendl (ε⁻¹.is-natural _ _ _) ⟩≡
L.₁ (ι.₁ g) ∘ ε⁻¹.η _ ∘ p₂' ∎

pb′ .p₁∘limiting =
pullr lpb.p₁∘limiting ∙ cancell (Lι-iso _ .is-invertible.invl)
pb′ .p₂∘limiting =
pullr lpb.p₂∘limiting ∙ 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