{-# OPTIONS --safe #-}
module Cubical.Categories.Site.Sieve where

-- Definition of sieves on an object
-- and the sieve generated by a cover.

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.Site.Cover

module _
  { ℓ' : Level}
  (C : Category  ℓ')
  where

  open Category C

  record Sieve (ℓsie : Level) (c : ob) : Type (ℓ-max  (ℓ-max ℓ' (ℓ-suc ℓsie))) where
    no-eta-equality
    field
      passes : {d : ob}  Hom[ d , c ]  Type ℓsie
      isPropPasses : {d : ob}  (f : Hom[ d , c ])  isProp (passes f)
      closedUnderPrecomposition :
        {d' d : ob} (p : Hom[ d' , d ]) (f : Hom[ d , c ]) 
        passes f  passes (p  f)


module _
  { ℓ' : Level}
  {C : Category  ℓ'}
  where

  open Category C hiding (_∘_)
  open Sieve

  sieveRefinesSieve :
    {ℓS' ℓS : Level} 
    {c : ob} 
    Sieve C ℓS' c 
    Sieve C ℓS c 
    Type (ℓ-max (ℓ-max (ℓ-max  ℓ') ℓS') ℓS)
  sieveRefinesSieve S' S =
    (d : ob) 
    (f : Hom[ d , _ ]) 
    passes S' f  passes S f

  isPropSieveRefinesSieve :
    {ℓS' ℓS : Level} 
    {c : ob} 
    (S : Sieve C ℓS' c) 
    (S' : Sieve C ℓS c) 
    isProp (sieveRefinesSieve S S')
  isPropSieveRefinesSieve S S' =
    isPropΠ3  d f _  isPropPasses S' f)

  generatedSieve : { : Level} {c : ob}  Cover C  c  Sieve C (ℓ-max ℓ' ) c
  passes (generatedSieve cov) f =
    ∃[ i   cov  ] Σ[ h  Hom[ _ , _ ] ] f  h  patchArr cov i
  isPropPasses (generatedSieve cov) f = isPropPropTrunc
  closedUnderPrecomposition (generatedSieve cov) p f =
    PT.rec isPropPropTrunc λ (i , h , f≡hi) 
         i
        , (p  h)
        , ( (p  f)                     ≡⟨ cong (p ⋆_) f≡hi 
            (p  (h  patchArr cov i))  ≡⟨ sym (⋆Assoc p h (patchArr cov i)) 
            ((p  h)  patchArr cov i)   )
      ∣₁

  coverRefinesSieve :
    {ℓcov ℓsie : Level}
    {c : ob} 
    Cover C ℓcov c 
    Sieve C ℓsie c 
    Type (ℓ-max ℓcov ℓsie)
  coverRefinesSieve cov S =
    (i : _)  passes S (patchArr cov i)

  isPropCoverRefinesSieve :
    {ℓcov ℓsie : Level}
    {c : ob} 
    (cov : Cover C ℓcov c) 
    (S : Sieve C ℓsie c) 
    isProp (coverRefinesSieve cov S)
  isPropCoverRefinesSieve _ S = isPropΠ  _  isPropPasses S _)

  coverRefinesGeneratedSieve :
    { : Level} 
    {c : ob} 
    {cov : Cover C  c} 
    coverRefinesSieve cov (generatedSieve cov)
  coverRefinesGeneratedSieve i =  i , id , sym (⋆IdL _) ∣₁

  -- The universal property of generatedSieve
  generatedSieveIsUniversal :
    {ℓcov ℓsie : Level} 
    {c : ob} 
    (cov : Cover C ℓcov c) 
    (S : Sieve C ℓsie c) 
    coverRefinesSieve cov S 
    sieveRefinesSieve (generatedSieve cov) S
  generatedSieveIsUniversal cov S cov≤S d f =
    PT.rec (isPropPasses S f)  (i , g , eq) 
      subst (passes S) (sym eq)
        (closedUnderPrecomposition S g (patchArr cov i) (cov≤S i)) )

  pulledBackSieve :
    {ℓsie : Level} 
    {c d : ob} 
    (Hom[ c , d ]) 
    Sieve C ℓsie d 
    Sieve C ℓsie c
  passes (pulledBackSieve f S) g = passes S (g  f)
  isPropPasses (pulledBackSieve f S) g = isPropPasses S _
  closedUnderPrecomposition (pulledBackSieve f S) p g pass =
    subst (passes S) (sym (⋆Assoc p g f))
      (closedUnderPrecomposition S p (g  f) pass)