{-# OPTIONS -vtactic.hlevel:30 #-}
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 where

module _ {o κ : _} (C : Precategory o κ) (c : ⌞ C ⌟) where
  private module C = Precategory C

Sieves🔗

Given a category $\mathcal{C}\text{,}$ a sieve on an object $c$ Is a subset of the maps $a\to c$ closed under composition: If $f\in S\text{,}$ then $(f\circ g)\in S\text{.}$ The data of a sieve on $c$ corresponds to the data of a subobject of $よ(c)\text{,}$ considered as an object of $\mathrm{PSh}(\mathcal{C})\text{.}$

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

  record Sieve : Type (o ⊔ κ) where
    field
      arrows : ∀ {y} → ℙ (C.Hom y c)
      closed : ∀ {y z f} (g : C.Hom y z) → f ∈ arrows → (f C.∘ g) ∈ arrows
  open Sieve public

instance
  Membership-Sieve : ∀ {o ℓ} {C : Precategory o ℓ} {c d} → Membership (C .Precategory.Hom d c) (Sieve C c) _
  Membership-Sieve = record { _∈_ = λ x S → x ∈ S .Sieve.arrows }

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

module _ {o κ : _} (C : Precategory o κ) (c : ⌞ C ⌟) where
  private
    module C   = Cat.Reasoning C
    module PSh = Cat.Reasoning (PSh κ C)

  open PSh._↪_
  open _=>_
  open Functor

  maximal' : Sieve C c
  maximal' .arrows x = ⊤Ω
  maximal' .closed g x = tt

  intersect : ∀ {I : Type κ} (F : I → Sieve C c) → Sieve C c
  intersect {I = I} F .arrows h = elΩ ((x : I) → h ∈ F x)
  intersect {I = I} F .closed g x = inc λ i → F i .closed g (□-out! x i)

Representing subfunctors🔗

Let $S$ be a sieve on $\mathcal{C}\text{.}$ We show that it determines a presheaf $S^{\prime }\text{,}$ and that this presheaf admits a monic natural transformation $S^{\prime }\hookrightarrow よ(c)\text{.}$ The functor determined by a sieve $S$ sends each object $d$ to the set of arrows $d\stackrel{f}{\to }c$ s.t. $f\in S\text{;}$ The functorial action is given by composition, as with the $\mathbf{Hom}$ functor.

  to-presheaf : Sieve C c → PSh.Ob
  to-presheaf sieve .F₀ d = el! (Σ[ f ∈ C.Hom d c ] (f ∈ sieve))
  to-presheaf sieve .F₁ f (g , s) = g C.∘ f , sieve .closed _ s

  to-presheaf sieve .F-id    = funext λ _ → Σ-prop-path! (C.idr _)
  to-presheaf sieve .F-∘ f g = funext λ _ → Σ-prop-path! (C.assoc _ _ _)

That this functor is a subobject of $よ$ follows straightforwardly: The injection map $S^{\prime }\hookrightarrow よ(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 C c} → 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 = ext λ i x → Σ-prop-path! (unext path i x)