un-bundle hProps in Sieve.agda

agda · Nov 17, 2023 · fa6a3a3 · fa6a3a3
1 parent 2eef94d
commit fa6a3a3
Show file tree

Hide file tree

Showing 2 changed files with 38 additions and 19 deletions.
diff --git a/Cubical/Categories/Site/Coverage.agda b/Cubical/Categories/Site/Coverage.agda
@@ -38,6 +38,6 @@ module _
         {d : ob} →
         (f : Hom[ d , c ]) →
         ∃[ cov' ∈ ⟨ covers d ⟩ ]
-          ⟨ coverRefinesSieve
-              (str (covers d) cov')
-              (pulledBackSieve f (generatedSieve (str (covers c) cov))) ⟩
+          coverRefinesSieve
+            (str (covers d) cov')
+            (pulledBackSieve f (generatedSieve (str (covers c) cov)))
diff --git a/Cubical/Categories/Site/Sieve.agda b/Cubical/Categories/Site/Sieve.agda
@@ -9,8 +9,6 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Structure
 
-open import Cubical.Functions.Logic using (∀[]-syntax; ∀[∶]-syntax; _⇒_; _⇔_)
-
 open import Cubical.HITs.PropositionalTruncation as PT
 
 open import Cubical.Data.Sigma
@@ -28,10 +26,11 @@ module _
   record Sieve (ℓsie : Level) (c : ob) : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc ℓsie))) where
     no-eta-equality
     field
-      passes : {d : ob} → Hom[ d , c ] → hProp ℓsie
+      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) ⟩
+        passes f → passes (p ⋆ f)
 
 
 module _
@@ -47,14 +46,25 @@ module _
     {c : ob} →
     Sieve C ℓS' c →
     Sieve C ℓS c →
-    hProp (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓS') ℓS)
+    Type (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓS') ℓS)
   sieveRefinesSieve S' S =
-    ∀[ d ∶ ob ] ∀[ f ∶ Hom[ d , _ ] ] (passes S' f ⇒ passes S f)
+    (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)
-    , isPropPropTrunc
+    ∃[ 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
@@ -69,15 +79,23 @@ module _
     {c : ob} →
     Cover C ℓcov c →
     Sieve C ℓsie c →
-    hProp (ℓ-max ℓcov ℓsie)
+    Type (ℓ-max ℓcov ℓsie)
   coverRefinesSieve cov S =
-    ∀[ i ] passes S (patchArr cov i)
+    (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) ⟩
+    coverRefinesSieve cov (generatedSieve cov)
   coverRefinesGeneratedSieve i = ∣ i , id , sym (⋆IdL _) ∣₁
 
   -- The universal property of generatedSieve
@@ -86,11 +104,11 @@ module _
     {c : ob} →
     (cov : Cover C ℓcov c) →
     (S : Sieve C ℓsie c) →
-    ⟨ coverRefinesSieve cov S ⟩ →
-    ⟨ sieveRefinesSieve (generatedSieve cov) S ⟩
+    coverRefinesSieve cov S →
+    sieveRefinesSieve (generatedSieve cov) S
   generatedSieveIsUniversal cov S cov≤S d f =
-    PT.rec (str (passes S f)) (λ (i , g , eq) →
-      subst (⟨_⟩ ∘ passes S) (sym eq)
+    PT.rec (isPropPasses S f) (λ (i , g , eq) →
+      subst (passes S) (sym eq)
         (closedUnderPrecomposition S g (patchArr cov i) (cov≤S i)) )
 
   pulledBackSieve :
@@ -100,6 +118,7 @@ module _
     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))
+    subst (passes S) (sym (⋆Assoc p g f))
       (closedUnderPrecomposition S p (g ⋆ f) pass)