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