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

private
  module C = Cat.Reasoning C
  module PSh = Cat.Reasoning (PSh κ C)
open PSh._↪_
open _=>_
open Functor

Sieves🔗

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

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 ⊔ 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 $a \to c$; It represents the identity map $よ(c) \to よ(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 = el ⊤ hlevel!
maximal′ .closed g x = tt

intersect : ∀ {I : Type κ} (F : I → Sieve) → Sieve
intersect {I = I} F .arrows h = elΩ ((x : I) → h ∈ F x .arrows)
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}$. We show that it determines a presheaf $S'$, and that this presheaf admits a monic natural transformation $S' \hookrightarrow よ(c)$. The functor determined by a sieve $S$ sends each object $d$ to the set of arrows $d \xrightarrow{f} c$ s.t. $f \in S$; The functorial action is given by composition, as with the $\mathbf{Hom}$ functor.

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

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

That this functor is a subobject of $よ$ follows straightforwardly: The injection map $S' \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} → 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) (path ηₚ x)