open import Cat.Instances.Functor
open import Cat.Functor.Hom
open import Cat.Prelude

open import Data.Power

import Cat.Reasoning

module Cat.Diagram.Sieve {o κ : _} (C : Precategory o κ) (c : Precategory.Ob C) where

Sieves🔗

Given a category C\ca{C}, a sieve on an object cc Is a subset of the maps aca \to c closed under composition: If fSf \in S, then (fg)S(f \circ g) \in S. The data of a sieve on cc corresponds to the data of a subobject of (c)\yo(c), considered as an object of PSh(C)\psh(\ca{C}).

Here, the subset is represented as the function arrows, which, given an arrow f:acf : a \to c (and its domain), yields a proposition representing inclusion in the subset.

record Sieve : Type (o  lsuc κ) where
  field
    arrows : {y : C.Ob}   (C.Hom y c)
    closed : {y z : _} {f : _} (g : C.Hom y z)
            f  arrows
            (f C.∘ g)  arrows
open Sieve

The maximal sieve on an object is the collection of all maps aca \to c; It represents the identity map (c)(c)\yo(c) \to \yo(c) as a subfunctor. A κ\kappa-small family of sieves can be intersected (the underlying predicate is the “κ\kappa-ary conjunction” Π\Pi — the universal quantifier), and this represents a wide pullback of subobjects.

maximal′ : Sieve
maximal′ .arrows x = Lift _  , λ _ _ _  lift tt
maximal′ .closed g x = lift tt

intersect :  {I : Type κ} (F : I  Sieve)  Sieve
intersect {I = I} F .arrows h =
    ((x : I)  h  F x .arrows)
  , Π-is-hlevel 1 λ _  F _ .arrows _ .is-tr
intersect {I = I} F .closed g x i = F i .closed g (x i)

Representing subfunctors🔗

Let SS be a sieve on C\ca{C}. We show that it determines a presheaf SS', and that this presheaf admits a monic natural transformation S(c)S' \mono \yo(c). The functor determined by a sieve SS sends each object dd to the set of arrows dfcd \xto{f} c s.t. fSf \in S; The functorial action is given by composition, as with the hom\hom functor.

to-presheaf : Sieve  PSh.Ob
to-presheaf sieve .F₀ d =
    Σ[ f  C.Hom d c ] (f  sieve .arrows)
  , Σ-is-hlevel 2 (C.Hom-set _ _) λ _  is-prop→is-set (sieve .arrows _ .is-tr)
to-presheaf sieve .F₁ f (g , s) = g C.∘ f , sieve .closed _ s

That this functor is a subobject of \yo follows straightforwardly: The injection map S(c)S' \mono \yo(c) is given by projecting out the first component, which is an embedding (since “being in a sieve” is a proposition). Since natural transformations are monic if they are componentwise monic, and embeddings are monic, the result follows.

to-presheaf↪よ : {S : Sieve}  to-presheaf S PSh.↪ よ₀ C c
to-presheaf↪よ {S} .mor .η x (f , _) = f
to-presheaf↪よ {S} .mor .is-natural x y f = refl
to-presheaf↪よ {S} .monic g h path = Nat-path λ x 
  embedding→monic (Subset-proj-embedding  _  S .arrows _ .is-tr))
    (g .η x) (h .η x) (ap  e  e .η x) path)