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

open import Data.Power

import Cat.Reasoning

open /-Obj

module Cat.Diagram.Sieve where

module _ {o ΞΊ : _} (C : Precategory o ΞΊ) (c : β C β) where
private module C = Precategory C


Sievesπ

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
no-eta-equality
field
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
private
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

instance
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' .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 _

  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 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

  abstract
pullback-id : β {c} {s : Sieve C c} β pullback C.id s β‘ s
pullback-id {s = s} = ext Ξ» h β Ξ©-ua
(subst (_β s) (C.idl h))
(subst (_β s) (sym (C.idl h)))

pullback-β
: β {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.

module _ {o β} (C : Precategory o β) where
open Precategory C using (Hom)

  record Cover (U : β C β) β' : Type (o β β β lsuc β') where
field
{index}  : Type β'
{domain} : index β β C β
map      : β i β Hom (domain i) U

open Cover

module _ {o β} {C : Precategory o β} where
private module C = Cat.Reasoning C
instance
Underlying-Cover : β {β' U} β Underlying (Cover C U β')
Underlying-Cover = record { β_β = index }


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.

  mapβsieve : β {V U} β C.Hom V U β Sieve C U
mapβsieve f .arrows g = elΞ© (Ξ£[ h β C.Hom _ _ ] (f C.β h β‘ g))
mapβsieve f .closed = rec! Ξ» g p h β inc (g C.β h , C.pulll p)

instance
β¦β§-Cover : β {β' U} β β¦β§-notation (Cover C U β')
β¦β§-Cover = brackets _ coverβsieve