Reasoning.lagda.md

```agda
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.

[overture on topos theory]: Topoi.Base.html

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.

```agda
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`{.Agda}), 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.

```agda
  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:

```agda
  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
```