open import 1Lab.Reflection.Copattern

open import Cat.Functor.FullSubcategory
open import Cat.Instances.Functor
open import Cat.Diagram.Sieve
open import Cat.Prelude hiding (glue)

import Cat.Functor.Reasoning.Presheaf as Psh
import Cat.Reasoning as Cat

module Cat.Site.Base where

private variable
  o ℓ ℓc ℓs : Level
  C : Precategory o ℓ

Sites and sheaves🔗

Sheaf theory is a particular formalisation of the idea that global structure $A(U)$ on a complicated object $U$ is often best studied at its restrictions to simpler parts $V_i$ which glue to recover $U\text{.}$ It’s particularly general, in the sense that the objects $U$ can belong to an arbitrary category $\mathcal{C}\text{,}$ as long as we equip $\mathcal{C}$ with structure (called a coverage) determining what we mean by glue together — and as long as our global structure $A(U)$ is fine living at the level of sets.

To make these ideas concrete, we will fix a category $\mathcal{C}$ of objects we want to study, and we will denote its objects by letters like $U\text{,}$ $V\text{,}$ and $W\text{.}$ The structures we will be interested in will all take the form of presheaves on $\mathcal{C}$ — functors into the category $\mathbf{Sets}\text{.}$ If we have any family of maps $(h_i:U_i\to U{)}_i\text{,}$ and an element $s:A(U)\text{,}$ then $A^{\prime }s$ functorial action ensures that we can restrict $s$ along the $h_i$ to obtain elements $s_i:A(U_i)\text{.}$

A representative example is when $\mathcal{C}$ is the frame $\Omega (L)$ underlying some locale $L\text{,}$ and the elements $U_i$ are such that $U={\bigvee }_i{U}_i\text{.}$ This setup has the particular geometric interpretation of expressing $U$ as a union of smaller parts. Extending this intuition, we would consider our original $s:A(U)$ to be the global information, and the restrictions $s_i:A(U_i)$ to be information local to a given sub-part of the whole $U\text{.}$

So far, we have said nothing new: this is simply functoriality. The interesting question is going the other way: if we have the local information $s_i:A(U_i)\text{,}$ can we glue them together to get the global information $s:A(U)\text{?}$ We can’t always: this might be a failure of the functor¹, or of the $s_i\text{.}$ While it might be a bit disheartening that there are notions of “information” which can not be put together locally, these failures tell us that we have a fruitful concept at hand.

First, assuming that our $s_i:A(U_i)$ are all restrictions of some $s:A(U)\text{,}$ we should investigate the properties it must have: these will tell us what properties we should impose on local data $t_i:A(V_i)$ to ensure it has a chance of gluing to a $t:A(V)\text{.}$ The key property is, once again, functoriality — but it also has a geometric interpretation. Suppose we have two objects $U_i$ and $U_j$ drawn from our family, and some arbitrary third object $V\text{,}$ and they fit into a commutative diagram like

If we are still thinking about $\mathcal{C}=\Omega (L)\text{,}$ then $V$ could simply be the intersection $U_i\cap U_j\text{,}$ and the diagram commutes automatically. In any case, we have two ways of restricting $s:A(U)$ to the intersection $V\text{,}$ namely $A(f)(s_i)$ and $A(g)(s_j)\text{.}$ By functoriality, we have

so that, if our “local” data comes from restricting “global” data, the local restrictions automatically agree on intersections. We thus have defined what it means to have local data with respect to a family of morphisms (which we think of as expressing their common codomain as being “glued together”), and what it means for that data to glue to give local data.

We could carry on and define sheaves from here, but we will make one final simplifying assumption: Instead of considering families of morphisms with common codomain, we will consider sieves in $\mathcal{C}\text{.}$ This lets us simplify the notion of compatibility: we now have values $s(f{h}_i)$ of $s$ at arbitrary composites of the $h_i\text{,}$ so that it suffices to demand $A(f)(s(h_i))=s(f{h}_i)\text{.}$

Terminology for local data🔗

-- Defining these notions for "non-functors" first will let us avoid
-- angering the positivity checker when defining sheafifications, see
-- that module for more details.
module pre {o ℓ ℓs} (C : Precategory o ℓ) {A₀ : ⌞ C ⌟ → Type ℓs} (A₁ : ∀ {U V} → C .Precategory.Hom U V → A₀ V → A₀ U) where
  open Precategory C

To formalise the notion of sheaf, we will need to introduce names for the ideas we’ve sketched out so far. First, if we are given a sieve $f_i:U_i\to U\text{,}$ we will refer to a family of elements $s(f_i):A(U_i)$ as a family of parts. If these parts satisfy the compatibility condition defined above, relative to the sieve $f_i\text{,}$ we will say they are a patch. The geometric intuition is key here: the $s(f_i)$ are to be the literal parts of some hypothetical $s:A(U)\text{,}$ and they’re a patch if they agree on the “intersections” $U_i\leftarrow V\to U_j\text{.}$

  Parts : ∀ {U} (T : Sieve C U) → Type _
  Parts {U} T = ∀ {V} (f : Hom V U) (hf : f ∈ T) → A₀ V

  is-patch : ∀ {U} (T : Sieve C U) (p : Parts T) → Type _
  is-patch {U} T part =
    ∀ {V W} (f : Hom V U) (hf : f ∈ T) (g : Hom W V) (hgf : f ∘ g ∈ T)
    → A₁ g (part f hf) ≡ part (f ∘ g) hgf

Finally, if we have a family $s(f_i):A(U_i)$ of parts, then we say that an element $s:A(U)$ is a section of these parts if its restriction along each $f_i$ agrees with the part $s(f_i)\text{:}$

  is-section : ∀ {U} (T : Sieve C U) → A₀ U → Parts T → Type _
  is-section {U = U} T s p =
    ∀ {V} (f : Hom V U) (hf : f ∈ T)
    → A₁ f s ≡ p f hf

module _ {o ℓ ℓs} {C : Precategory o ℓ} (A : Functor (C ^op) (Sets ℓs)) where
  open Precategory C
  private module A = Psh A
  open pre C A.₁ hiding (is-section)

We will most often consider parts-which-are-patches, so we introduce a record type to bundle them; similarly, we will consider elements-which-are-sections, so they also get a record type.

  record Patch {U} (T : Sieve C U) : Type (o ⊔ ℓ ⊔ ℓs) where
    no-eta-equality
    field
      part  : Parts T
      patch : is-patch T part

    abstract
      app : ∀ {V} {f g : Hom V U} {hf hg} → f ≡ g → part f hf ≡ part g hg
      app p = ap₂ part p prop!

      compatible
        : ∀ {V W X} {i : Hom W U} {j : Hom X U} (g : Hom V W) (h : Hom V X)
        → {is : i ∈ T} {js : j ∈ T}
        → i ∘ g ≡ j ∘ h
        → A ⟪ g ⟫ part i is ≡ A ⟪ h ⟫ part j js
      compatible {i = i} {j} g h {is} {js} p =
        A ⟪ g ⟫ part i is ≡⟨ patch i _ g (T .closed is g) ⟩≡
        part (i ∘ g) _    ≡⟨ app p ⟩≡
        part (j ∘ h) _    ≡⟨ sym (patch j _ h (T .closed js h)) ⟩≡
        A ⟪ h ⟫ part j js ∎

  open Patch

  is-section : ∀ {U} {T : Sieve C U} → A ʻ U → Patch T → Type _
  is-section {T = T} p x = pre.is-section C A.₁ T p (x .part)

  record Section {U} {T : Sieve C U} (p : Patch T) : Type (o ⊔ ℓ ⊔ ℓs) where
    no-eta-equality
    field
      {whole} : A ʻ U
      glues   : is-section whole p

module _ {o ℓ ℓs} {C : Precategory o ℓ} {A : Functor (C ^op) (Sets ℓs)} where
  open Cat C
  open Section
  open Patch
  private module A = Psh A
  open pre C A.₁ hiding (is-section) public

  instance
    Extensional-Patch
      : ∀ {U ℓr} {S : Sieve C U} ⦃ _ : Extensional (Parts S) ℓr ⦄
      → Extensional (Patch A S) ℓr
    Extensional-Patch ⦃ e ⦄ .Pathᵉ x y = e .Pathᵉ (x .part) (y .part)
    Extensional-Patch ⦃ e ⦄ .reflᵉ x = e .reflᵉ (x .part)
    Extensional-Patch ⦃ e ⦄ .idsᵉ .to-path p i .part = e .idsᵉ .to-path p i
    Extensional-Patch ⦃ e ⦄ .idsᵉ .to-path {x} {y} p i .patch {W = W} f hf g hgf =
      is-prop→pathp (λ i → A.₀ W .is-tr (A.₁ g (e .idsᵉ .to-path p i _ hf)) (e .idsᵉ .to-path p i _ hgf))
        (x .patch f hf g hgf) (y .patch f hf g hgf) i
    Extensional-Patch ⦃ e ⦄ .idsᵉ .to-path-over p = is-prop→pathp (λ i → Pathᵉ-is-hlevel  e (hlevel )) _ _

    Extensional-Section
      : ∀ {U ℓr} {S : Sieve C U} {p : Patch A S} ⦃ _ : Extensional (A ʻ U) ℓr ⦄
      → Extensional (Section A p) ℓr
    Extensional-Section ⦃ e ⦄ .Pathᵉ x y = e .Pathᵉ (x .whole) (y .whole)
    Extensional-Section ⦃ e ⦄ .reflᵉ x = e .reflᵉ (x .whole)
    Extensional-Section ⦃ e ⦄ .idsᵉ .to-path p i .whole = e .idsᵉ .to-path p i
    Extensional-Section {p = p} ⦃ e ⦄ .idsᵉ .to-path {a} {b} q i .glues {V} f hf =
      is-prop→pathp (λ i → A.₀ V .is-tr (A.₁ f (e .idsᵉ .to-path q i)) (p .part f hf))
        (a .glues f hf) (b .glues f hf) i
    Extensional-Section ⦃ e ⦄ .idsᵉ .to-path-over p = is-prop→pathp (λ i → Pathᵉ-is-hlevel  e (hlevel )) _ _

  subset→patch
    : ∀ {U} {S S' : Sieve C U}
    → S' ⊆ S
    → Patch A S
    → Patch A S'
  subset→patch incl p .part f hf = p .part f (incl f hf)
  subset→patch incl p .patch f hf g hgf = p .patch f _ g _

  pullback-patch : ∀ {U V} {S : Sieve C U} (f : Hom V U) → Patch A S → Patch A (pullback f S)
  pullback-patch {S = S} f s .part g p = s .part (f ∘ g) p
  pullback-patch {S = S} f s .patch g h hfg hfgh =
      s .patch (f ∘ g) h hfg (S .closed h hfg)
    ∙ app s (pullr refl)

  open _=>_

  map-patch
    : ∀ {B : Functor (C ^op) (Sets ℓs)} {U} {S : Sieve C U} (eta : A => B)
    → Patch A S
    → Patch B S
  map-patch eta x .part f hf = eta .η _ (x .part f hf)
  map-patch eta x .patch f hf g hgf = sym (eta .is-natural _ _ _ $ₚ _) ∙ ap (eta .η _) (x .patch f hf g hgf)

Finally, we will formalise the idea that any global information $s:A(U)$ can be made into a bunch of local pieces by restricting functorially.

  section→patch : ∀ {U} {T : Sieve C U} → A ʻ U → Patch A T
  section→patch x .part  f _ = A ⟪ f ⟫ x
  section→patch x .patch f hf g hgf = A.collapse refl

  section→section
    : ∀ {U} {T : Sieve C U} (u : A ʻ U)
    → Section A {T = T} (section→patch u)
  section→section u .whole      = u
  section→section u .glues f hf = refl

The notion of sheaf🔗

Using our terminology above, we can very concisely define what it means for a functor $A:\mathrm{PSh}(\mathcal{C})$ to be a sheaf, at least with respect to a sieve $T$ on $U\text{:}$ any patch $p$ of $T$ has a unique section. Thinking intuitively, satisfying the sheaf condition for a sieve $T$ means that each $s:A(U)$ arises uniquely as the gluing of some patch $s(f_i):A(U_i)\text{.}$

module _ {o ℓ ℓs} {C : Precategory o ℓ} (A : Functor (C ^op) (Sets ℓs)) where
  open Precategory C
  open Section
  open Patch

  is-sheaf₁ : ∀ {U} (T : Sieve C U) → Type _
  is-sheaf₁ T = (p : Patch A T) → is-contr (Section A p)

  is-separated₁ : ∀ {U} (T : Sieve C U) → Type _
  is-separated₁ {U} T =
    ∀ {x y : A ʻ U}
    → (∀ {V} (f : Hom V U) (hf : f ∈ T) → A ⟪ f ⟫ x ≡ A ⟪ f ⟫ y)
    → x ≡ y

Note that every sheaf is indeed separated, even after this unfolding, using the above mapping from elements to sections. The assumption of “$T\text{-local}$ equality” is exactly what we need to assure that $y$ is also a section of the patch generated by restricting $x\text{.}$

  is-sheaf₁→is-separated₁ : ∀ {U} (T : Sieve C U) → is-sheaf₁ T → is-separated₁ T
  is-sheaf₁→is-separated₁ T sheaf {x} {y} lp = ap whole $
    let
      sec₁ : Section A (section→patch x)
      sec₁ = section→section x

      sec₂ : Section A (section→patch x)
      sec₂ = record
        { whole = y
        ; glues = λ f hf →
          A ⟪ f ⟫ y ≡˘⟨ lp f hf ⟩≡˘
          A ⟪ f ⟫ x ∎
        }
    in is-contr→is-prop (sheaf (section→patch x)) sec₁ sec₂

  from-is-separated₁
    : ∀ {U} {T : Sieve C U}
    → is-separated₁ T
    → ∀ {p : Patch A T} (s : Section A p)
    → is-contr (Section A p)
  from-is-separated₁ sep sec .centre = sec
  from-is-separated₁ sep sec .paths x = ext $ sep λ f hf →
    sec .glues f hf ∙ sym (x .glues f hf)

  -- This is equal to `subst (is-sheaf₁ A)` but has better definitional
  -- behaviour for the relevant part.
  subst-is-sheaf₁ : ∀ {U} {T S : Sieve C U} (p : T ≡ S) → is-sheaf₁ T → is-sheaf₁ S
  subst-is-sheaf₁ {T = T} {S = S} p shf pa = done where
    pa' : Patch A T
    pa' .part f hf = pa .part f (subst (f ∈_) p hf)
    pa' .patch f hf g hgf = pa .patch f _ g _

    sec = shf pa'

    done : is-contr (Section A pa)
    done .centre .whole = sec .centre .whole
    done .centre .glues f hf = sec .centre .glues f (subst (f ∈_) (sym p) hf) ∙ app pa refl
    done .paths x = ext (ap whole (sec .paths record { glues = λ f hf → x .glues f (subst (f ∈_) p hf) ∙ app pa refl }))

Sites, formally🔗

Up until now, we have only been considering single sieves $f_i:U_i\to U$ when defining parts, patches, sections and sheaves. But a given category, even the opens of a locale, will generally have many distinct sieves on $U$ which could equally well be taken to be decompositions of $U$. We would like a sheaf “on $\mathcal{C}$” to have the local-to-global property for all of these decompositions, but we need to impose some order to make sure that we end up with a well-behaved category of sheaves.

We define a coverage $J$ on $\mathcal{C}$ to consist of, for each $U:\mathcal{C}\text{,}$ a family $J(U)$ of covering sieves on $U\text{.}$ Translating this into type theory, for each $U\text{,}$ we have a type $J(U)$ of “$J\text{-covers}$ of $U$”, and, for each $x:J(U)\text{,}$ we have an associated sieve $J(x)$ on $U\text{.}$

record Coverage {o ℓ} (C : Precategory o ℓ) ℓc : Type (o ⊔ ℓ ⊔ lsuc ℓc) where
  no-eta-equality

  open Precategory C

  field
    covers : ⌞ C ⌟ → Type ℓc
    cover  : ∀ {U} → covers U → Sieve C U

The $J(U)$ must satisfy the following stability property: if $R:J(U)$ is some covering sieve, and $f:V\to U$ is an arbitrary morphism, then there merely exists a covering sieve $S:J(V)$ which is contained in the pullback sieve $f^{\ast }(R)\text{.}$ The quantifier complexity for this statement is famously befuddling, but stating it in terms of sieves does simplify the formalisation:

    stable
      : ∀ {U V : ⌞ C ⌟} (R : covers U) (f : Hom V U)
      → ∃[ S ∈ covers V ] (cover S ⊆ pullback f (cover R))

Thinking back to the case of $\mathcal{C}=\Omega (L)\text{,}$ we can equip any frame with a coverage. The stability condition, in that case, reduces to showing that, if a family $U_i\hookrightarrow U$ has all of $U$ as its union, then the family $(U_i\cap V)\hookrightarrow (U\cap V)$ has $U\cap V$ as its union.

open Coverage public

instance
  Funlike-Coverage : Funlike (Coverage C ℓc) ⌞ C ⌟ (λ _ → Type ℓc)
  Funlike-Coverage = record { _#_ = λ C U → C .covers U }

  Membership-Coverage : ∀ {U} → Membership (Coverage C ℓc) (Sieve C U) _
  Membership-Coverage = record { _∈_ = λ C S → fibre (C .cover) S }

module _ {o ℓ ℓc ℓs} {C : Precategory o ℓ} (J : Coverage C ℓc) (A : Functor (C ^op) (Sets ℓs)) where

Finally, we (re-)define separated presheaves and sheaves with respect to a coverage $J\text{.}$ For separated presheaves, we can simply reuse the definition given above, demanding it for every $J\text{-covering}$ sieve. But for sheaves, formalisation concerns lead us to instead define an “unpacked” record type:

  is-separated : Type _
  is-separated = ∀ {U : ⌞ C ⌟} (c : J # U) → is-separated₁ A (J .cover c)

  record is-sheaf : Type (o ⊔ ℓ ⊔ ℓs ⊔ ℓc) where
    no-eta-equality
    field
      whole   : ∀ {U} (S : J .covers U) (p : Patch A (J .cover S)) → A ʻ U
      glues   : ∀ {U} (S : J .covers U) (p : Patch A (J .cover S)) → is-section A (whole S p) p
      separate : is-separated

This splitting of the sheaf condition into an operation and laws will help us in defining sheafifications later on. We can package the first two fields as saying that each patch has a section:

    split : ∀ {U} {S : J .covers U} (p : Patch A (J .cover S)) → Section A p
    split p .Section.whole = whole _ p
    split p .Section.glues = glues _ p

  open is-sheaf using (whole ; glues ; separate) public

Note that, if a functor satisfies the sheaf condition for all $J\text{-covering}$ sieves, it’s also a sheaf relative to quite a few other sieves: these are the closure properties of sites.

module _ {o ℓ ℓc ℓs} {C : Precategory o ℓ} {J : Coverage C ℓc} {A : Functor (C ^op) (Sets ℓs)} where
  from-is-separated
    : is-separated J A
    → (∀ {U} (c : J .covers U) (s : Patch A (J .cover c)) → Section A s)
    → is-sheaf J A
  from-is-separated sep split .whole S p  = split S p .Section.whole
  from-is-separated sep split .glues S p  = split S p .Section.glues
  from-is-separated sep split .separate S = sep S

  from-is-sheaf₁
    : (∀ {U} (c : J .covers U) → is-sheaf₁ A (J .cover c))
    → is-sheaf J A
  from-is-sheaf₁ shf .whole S p = shf _ p .centre .Section.whole
  from-is-sheaf₁ shf .glues S p = shf _ p .centre .Section.glues
  from-is-sheaf₁ shf .separate S = is-sheaf₁→is-separated₁ _ _ (shf _)

  to-is-sheaf₁ : is-sheaf J A → ∀ {U} (c : J .covers U) → is-sheaf₁ A (J .cover c)
  to-is-sheaf₁ shf c p = from-is-separated₁ _ (shf .separate c) (is-sheaf.split shf p)

open Section public
open Patch public

module _ {o ℓ ℓc ℓp} {C : Precategory o ℓ} {J : Coverage C ℓc} {A : Functor (C ^op) (Sets ℓp)} where
  private unquoteDecl eqv = declare-record-iso eqv (quote is-sheaf)
  abstract instance
    H-Level-is-sheaf : ∀ {n} → H-Level (is-sheaf J A) (suc n)
    H-Level-is-sheaf = prop-instance $ retract→is-hlevel  from to ft (hlevel ) where
      T : Type (o ⊔ ℓ ⊔ ℓc ⊔ ℓp)
      T = ∀ {U} (S : J .covers U) (p : Patch A (J .cover S)) → is-contr (Section A p)

      from : T → is-sheaf J A
      from x .whole S p  = x S p .centre .whole
      from x .glues S p  = x S p .centre .glues
      from x .separate S = is-sheaf₁→is-separated₁ A _ (x S)

      to : is-sheaf J A → T
      to shf S p = from-is-separated₁ _ (shf .separate S) (is-sheaf.split shf p)

      ft : ∀ x → from (to x) ≡ x
      ft x = Iso.injective eqv (Σ-prop-path! refl)

module _ {o ℓ ℓc} {C : Precategory o ℓ} (J : Coverage C ℓc) ℓs where
  open Precategory
  open Functor

We will often refer to a category $\mathcal{C}$ with a coverage $J$ as the site $(\mathcal{C},J)\text{.}$ The first notion we define relative to sites is the category of sheaves on a site, $\mathrm{Sh}(\mathcal{C},J)\text{:}$ the full subcategory of the presheaves on $\mathcal{C}$ which are $J\text{-sheaves.}$ The nature of the sheaf condition ensures that $\mathrm{Sh}(\mathcal{C},J)$ inherits most of $\mathrm{PSh}(\mathcal{C})\text{’s}$ good categorical properties — we refer to it as the topos of sheaves.

  Sheaf : Type _
  Sheaf = Σ[ p ∈ Functor (C ^op) (Sets ℓs) ] is-sheaf J p

  Sheaves : Precategory (o ⊔ ℓ ⊔ ℓc ⊔ lsuc ℓs) (o ⊔ ℓ ⊔ ℓs)
  unquoteDef Sheaves = define-copattern Sheaves $
    Restrict {C = PSh ℓs C} (is-sheaf J)

  forget-sheaf : Functor Sheaves (PSh ℓs C)
  forget-sheaf .F₀ (S , _) = S
  forget-sheaf .F₁ f = f
  forget-sheaf .F-id = refl
  forget-sheaf .F-∘ f g = refl