Sieves in categories

module category-theory.sieves-categories where
Imports
open import category-theory.categories

open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

A sieve S on an object X in a category C is a collection of morphisms into X which is closed under precomposition by arbitrary morphisms of C. In other words, for any morphism f : Y → X in S and any morphism g : Z → Y in C, the morphism f ∘ g : Z → X is in S.

The notion of sieve generalizes simultaneously the notion of right ideal in a monoid (a one-object category) and a lower set in a poset (a category with at most one morphism between any two objects).

Definition

module _
  {l1 l2 : Level} (C : Category l1 l2) (A : obj-Category C)
  where

  is-sieve-Category-Prop :
    { l3 : Level}
    ( S : (X Y : obj-Category C) 
    subtype l3 (type-hom-Category C X Y))  Prop (l1  l2  l3)
  is-sieve-Category-Prop S =
    Π-Prop
      ( obj-Category C)
      ( λ X 
        Π-Prop
          ( obj-Category C)
          ( λ Y 
            Π-Prop
              ( obj-Category C)
              ( λ Z 
                Π-Prop
                  ( type-subtype (S Y X))
                  ( λ f 
                    Π-Prop
                      ( type-hom-Category C Z Y)
                      ( λ g 
                        S Z X
                          ( comp-hom-Category
                              C (inclusion-subtype (S Y X) f) g))))))

  is-sieve-Category :
    { l3 : Level}
    ( S : (X Y : obj-Category C) 
    subtype l3 (type-hom-Category C X Y))  UU (l1  l2  l3)
  is-sieve-Category S = type-Prop (is-sieve-Category-Prop S)

  is-prop-is-sieve-Category :
    { l3 : Level}
    ( S : (X Y : obj-Category C)  subtype l3 (type-hom-Category C X Y)) 
    is-prop (is-sieve-Category S)
  is-prop-is-sieve-Category S = is-prop-type-Prop (is-sieve-Category-Prop S)