{-# OPTIONS --safe #-}
module Cubical.Categories.Site.Sieve where
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 _) ∣₁
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)