module Cat.Site.Constructions where

Constructing sitesπŸ”—

This module collects miscellaneous helpers for constructing sites. The first thing we observe is that we can form a coverage by considering a pullback-stable predicate, rather than pullback-stable families. This is the usual fibration/family dichotomy.

from-stable-property
  : βˆ€ {o β„“ β„“j} {C : Precategory o β„“}
  β†’ (P : βˆ€ {U} β†’ Sieve C U β†’ Type β„“j)
  β†’ (βˆ€ {U V} (f : C .Precategory.Hom V U) (s : Sieve C U) β†’ P s β†’ P (pullback f s))
  β†’ Coverage C (o βŠ” β„“ βŠ” β„“j)
from-stable-property P stab .covers U = Σ[ s ∈ Sieve _ U ] P s
from-stable-property P stab .cover = fst
from-stable-property P stab .stable (S , ps) f = pure
  ((pullback f S , stab f S ps) , Ξ» g hf β†’ hf)

In a similar vein, we can generalise from families of sieves to families of families, since every family generates a sieve. We call a presentation of a Coverage in terms of families-of-families a family of Coverings, since Agda forces us to differentiate the names.

  record Coverings β„“i β„“c : Type (o βŠ” β„“ βŠ” lsuc (β„“i βŠ” β„“c)) where
    field
      covers : ⌞ C ⌟ β†’ Type β„“i
      family : βˆ€ {U} β†’ covers U β†’ Cover C U β„“c

The definition of the stability property can be simplified slightly, by quantifying over the family rather than over the sieve it generates.

      stable
        : βˆ€ {U V} (S : covers U) (f : C .Hom V U) β†’ βˆƒ[ R ∈ covers V ]
          (βˆ€ i β†’ family R .map i ∈ pullback f ⟦ family S ⟧)

It’s not very complicated to show that this simplified stability property implies the literal stability property for the generated sieves.

  from-families : βˆ€ {β„“i β„“f} β†’ Coverings C β„“i β„“f β†’ Coverage C β„“i
  from-families cov .covers  = cov .covers
  from-families cov .cover S = ⟦ cov .family S ⟧
  from-families cov .stable S f = do
    (R , incl) ← cov .stable S f
    let
      incl' : ⟦ cov .family R ⟧ βŠ† pullback f ⟦ _ ⟧
      incl' {W} = elim! Ξ» g r h p β†’ do
        (s , i , q) ← incl r
        pure (s , i ∘ h , extendl q βˆ™ ap (f ∘_) p)
    pure (R , incl')