module Cat.Diagram.Sieve where


Given a category a sieve on an object Is a subset of the maps closed under composition: If then The data of a sieve on corresponds to the data of a subobject of considered as an object of

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

  record Sieve : Type (o βŠ” ΞΊ) where
      arrows : βˆ€ {y} β†’ β„™ (C.Hom y c)
      closed : βˆ€ {y z f} (hf : f ∈ arrows) (g : C.Hom y z) β†’ (f C.∘ g) ∈ arrows
  open Sieve public

The maximal sieve on an object is the collection of all maps It represents the identity map as a subfunctor. A family of sieves can be intersected (the underlying predicate is the β€œ conjunction” β€” the universal quantifier), and this represents a wide pullback of subobjects.

module _ {o β„“ : _} {C : Precategory o β„“} where
    module C   = Cat.Reasoning C
    module PSh = Cat.Reasoning (PSh β„“ C)
    open Precategory C

  Sieve-path : βˆ€ {c} {x y : Sieve C c} β†’ Path (βˆ€ {y} β†’ β„™ (C.Hom y c)) (x .arrows) (y .arrows) β†’ x ≑ y
  Sieve-path {x = x} {y} p i .arrows = p i
  Sieve-path {x = x} {y} p i .closed {f = f} hf g =
    is-propβ†’pathp (Ξ» i β†’ fun-is-hlevel {A = ⌞ p i f ⌟} 1 (p i (f ∘ g) .is-tr)) (Ξ» w β†’ x .closed w g) (Ξ» w β†’ y .closed w g) i hf

    hom∈Sieve : βˆ€ {c d} β†’ Membership (C.Hom d c) (Sieve C c) _
    hom∈Sieve = record { _∈_ = Ξ» x S β†’ x ∈ S .Sieve.arrows }

    slice∈Sieve : βˆ€ {c} β†’ Membership (/-Obj {C = C} c) (Sieve C c) _
    slice∈Sieve = record { _∈_ = Ξ» x S β†’ x .map ∈ S }

    Inclusion-sieve : βˆ€ {U} β†’ Inclusion (Sieve C U) _
    Inclusion-sieve {U} = record { _βŠ†_ = Ξ» S T β†’ βˆ€ {V} (h : Hom V U) β†’ h ∈ S β†’ h ∈ T }

    Extensional-sieve : βˆ€ {β„“r c} ⦃ _ : Extensional (βˆ€ {y} β†’ C.Hom y c β†’ Ξ©) β„“r ⦄ β†’ Extensional (Sieve C c) β„“r
    Extensional-sieve ⦃ e ⦄ = injectionβ†’extensional! Sieve-path e

    H-Level-Sieve : βˆ€ {c n} β†’ H-Level (Sieve C c) (2 + n)
    H-Level-Sieve = basic-instance 2 $
      embedding→is-hlevel 1 (injective→is-embedding! Sieve-path) (hlevel 2)

  open PSh._β†ͺ_
  open _=>_
  open Functor
  maximal' : βˆ€ {c} β†’ Sieve C c
  maximal' .arrows x = ⊀Ω
  maximal' .closed g x = tt

  intersect : βˆ€ {c} {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 x g = inc Ξ» i β†’ F i .closed (β–‘-out! x i) g

Representing subfunctorsπŸ”—

Let be a sieve on We show that it determines a presheaf and that this presheaf admits a monic natural transformation The functor determined by a sieve sends each object to the set of arrows s.t. The functorial action is given by composition, as with the functor.

  to-presheaf : βˆ€ {c} β†’ Sieve C c β†’ PSh.Ob
  to-presheaf {c} sieve .Fβ‚€ d = el! (Ξ£[ f ∈ C.Hom d c ] (f ∈ sieve))
  to-presheaf sieve .F₁ f (g , s) = g C.∘ f , sieve .closed s _

That this functor is a subobject of follows straightforwardly: The injection map 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β†ͺγ‚ˆ : βˆ€ {c} {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)

Pullback of sievesπŸ”—

If we have a sieve on and any morphism then there is a natural way to restrict the to a sieve on a morphism belongs to the restriction if the composite belongs to We refer to the resulting sieve as the pullback of along , and write it

  pullback : βˆ€ {u v} β†’ C.Hom v u β†’ Sieve C u β†’ Sieve C v
  pullback f s .arrows h = el (f C.∘ h ∈ s) (hlevel 1)
  pullback f s .closed hf g = subst (_∈ s) (sym (C.assoc f _ g)) (s .closed hf g)

If we consider the collection of β€œsieves on ” as varying along as a parameter, the pullback operation becomes functorial. Since it is contravariant, this means that the assignment is itself a presheaf on

    pullback-id : βˆ€ {c} {s : Sieve C c} β†’ pullback s ≑ s
    pullback-id {s = s} = ext Ξ» h β†’ Ξ©-ua
      (subst (_∈ s) (C.idl h))
      (subst (_∈ s) (sym (C.idl h)))

      : βˆ€ {u v w} {f : C.Hom w v} {g : C.Hom v u} {R : Sieve C u}
      β†’ pullback (g C.∘ f) R ≑ pullback f (pullback g R)
    pullback-∘ {f = f} {g} {R = R} = ext Ξ» h β†’ Ξ©-ua
      (subst (_∈ R) (sym (C.assoc g f h)))
      (subst (_∈ R) (C.assoc g f h))

This presheaf has an important universal property: the natural transformations correspond naturally to the subobjects of Categorically, we say that is a subobject classifier in the category

  Sieves : Functor (C ^op) (Sets (o βŠ” β„“))
  Sieves .Fβ‚€ U .∣_∣ = Sieve C U
  Sieves .Fβ‚€ U .is-tr = hlevel 2
  Sieves .F₁ = pullback
  Sieves .F-id    = funext Ξ» x β†’ pullback-id
  Sieves .F-∘ f g = funext Ξ» x β†’ pullback-∘

Generated sievesπŸ”—

Often, it’s more practical to define a family of maps, and to obtain a sieve from this family after the fact. To this end, we define a type Cover for families of maps into a common codomain, paired with their indexing type.

  record Cover (U : ⌞ C ⌟) β„“' : Type (o βŠ” β„“ βŠ” lsuc β„“') where
      {index}  : Type β„“'
      {domain} : index β†’ ⌞ C ⌟
      map      : βˆ€ i β†’ Hom (domain i) U

The sieve generated by a cover is the collection of maps that factor through at least one of the i.e., for a map it is the proposition

  coverβ†’sieve : βˆ€ {β„“' U} β†’ Cover C U β„“' β†’ Sieve C U
  cover→sieve {U = U} f .arrows {W} g = elΩ do
    Ξ£[ i ∈ f ] Ξ£[ h ∈ C.Hom W (f .domain i) ] (f .map i C.∘ h ≑ g)
  coverβ†’sieve f .closed = rec! Ξ» i h p g β†’ inc (i , h C.∘ g , C.pulll p)

Since the primary purpose of Cover is to present sieves, we register an instance of the ⟦⟧-notation class, so that we can write ⟦ cov ⟧ instead of coverβ†’sieve cov.