rename F -> sheafification

Cubical/Categories/Site/Sheafification/Base.agda

@@ -106,21 +106,21 @@ module Sheafification
       (patch : ⟨ cov ⟩) →
       restrict (patchArr cov patch) (amalgamate cover fam) ≡ fst fam patch
 
-  F : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
-  Functor.F-ob F c = ⟨F⟅ c ⟆⟩ , trunc
-  Functor.F-hom F = restrict
-  Functor.F-id F = funExt restrictId
-  Functor.F-seq F f g = funExt (restrictRestrict f g)
-
-  isSheafF : isSheaf J F
-  isSheafF c cover = isEmbedding×isSurjection→isEquiv
+  sheafification : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP)
+  Functor.F-ob sheafification c = ⟨F⟅ c ⟆⟩ , trunc
+  Functor.F-hom sheafification = restrict
+  Functor.F-id sheafification = funExt restrictId
+  Functor.F-seq sheafification f g = funExt (restrictRestrict f g)
+
+  isSheafSheafification : isSheaf J sheafification
+  isSheafSheafification c cover = isEmbedding×isSurjection→isEquiv
     ( injEmbedding
-        (isSetCompatibleFamily F cov)
+        (isSetCompatibleFamily sheafification cov)
         (λ {x} {y} x~y → sep cover x y (funExt⁻ (cong fst x~y)))
     , λ fam →
         ∣ amalgamate cover fam
         , Σ≡Prop
-            (isPropIsCompatibleFamily F cov)
+            (isPropIsCompatibleFamily sheafification cov)
             (funExt (restrictAmalgamate cover fam)) ∣₁ )
     where
     cov = str (covers c) cover

Cubical/Categories/Site/Sheafification/ElimProp.agda

@@ -36,12 +36,12 @@ module _
   -- We name the (potential) assumptions on 'B' here to avoid repetition.
   module ElimPropAssumptions
     {ℓB : Level}
-    (B : {c : ob} → ⟨F⟅ c ⟆⟩ → Type ℓB)
+    (B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB)
     where
 
     isPropValued =
       {c : ob} →
-      {x : ⟨F⟅ c ⟆⟩} →
+      {x : ⟨ sheafification ⟅ c ⟆ ⟩} →
       isProp (B x)
 
     Onη =
@@ -53,7 +53,7 @@ module _
     -- should usually be more convenient to prove.
     isLocal =
       {c : ob} →
-      (x : ⟨F⟅ c ⟆⟩) →
+      (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
       (cover : ⟨ covers c ⟩) →
       let cov = str (covers c) cover in
       ((patch : ⟨ cov ⟩) → B (restrict (patchArr cov patch) x)) →
@@ -63,15 +63,15 @@ module _
     isMonotonous =
       {c d : ob} →
       (f : Hom[ d , c ]) →
-      (x : ⟨F⟅ c ⟆⟩) →
+      (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
       B x → B (restrict f x)
 
   open ElimPropAssumptions
 
   -- A fist version of elimProp that uses the isMonotonous assumption.
   module ElimPropWithMonotonous
     {ℓB : Level}
-    {B : {c : ob} → ⟨F⟅ c ⟆⟩ → Type ℓB}
+    {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
     (isPropValuedB : isPropValued B)
     (onηB : Onη B)
     (isLocalB : isLocal B)
@@ -84,7 +84,7 @@ module _
       {c : ob} →
       (cover : ⟨ covers c ⟩) →
       let cov = str (covers c) cover in
-      (fam : CompatibleFamily F cov) →
+      (fam : CompatibleFamily sheafification cov) →
       ((patch : ⟨ cov ⟩) → B (fst fam patch)) →
       B (amalgamate cover fam)
     amalgamatePreservesB cover fam famB =
@@ -96,14 +96,14 @@ module _
     -- A helper to deal with the path constructor cases.
     mkPathP :
       {c : ob} →
-      {x0 x1 : ⟨F⟅ c ⟆⟩} →
+      {x0 x1 : ⟨ sheafification ⟅ c ⟆ ⟩} →
       (p : x0 ≡ x1) →
       (b0 : B (x0)) →
       (b1 : B (x1)) →
       PathP (λ i → B (p i)) b0 b1
     mkPathP p = isProp→PathP (λ i → isPropValuedB)
 
-    elimProp : {c : ob} → (x : ⟨F⟅ c ⟆⟩) → B x
+    elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
     elimProp (trunc x y p q i j) =
       isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropValuedB)
         (elimProp x)
@@ -151,15 +151,15 @@ module _
   -- Now we drop the 'isMonotonous' assumption and prove the stronger version of 'elimProp'.
   module _
     {ℓB : Level}
-    {B : {c : ob} → ⟨F⟅ c ⟆⟩ → Type ℓB}
+    {B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type ℓB}
     (isPropValuedB : isPropValued B)
     (onηB : Onη B)
     (isLocalB : isLocal B)
     where
 
     -- Idea: strengthen the inductive hypothesis to "every restriction of x satisfies 'B'"
     private
-      B' : {c : ob} → ⟨F⟅ c ⟆⟩ → Type (ℓ-max (ℓ-max ℓ ℓ') ℓB)
+      B' : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type (ℓ-max (ℓ-max ℓ ℓ') ℓB)
       B' x = {d : ob} → (f : Hom[ d , _ ]) → B (restrict f x)
 
       isPropValuedB' : isPropValued B'
@@ -195,7 +195,7 @@ module _
 
       elimPropInduction :
         {c : ob} →
-        (x : ⟨F⟅ c ⟆⟩) →
+        (x : ⟨ sheafification ⟅ c ⟆ ⟩) →
         B' x
       elimPropInduction =
         ElimPropWithMonotonous.elimProp {B = B'}
@@ -204,5 +204,5 @@ module _
           isLocalB'
           isMonotonousB'
 
-    elimProp : {c : ob} → (x : ⟨F⟅ c ⟆⟩) → B x
+    elimProp : {c : ob} → (x : ⟨ sheafification ⟅ c ⟆ ⟩) → B x
     elimProp x = subst B (restrictId _) (elimPropInduction x id)

Cubical/Categories/Site/Sheafification/UniversalProperty.agda

@@ -32,7 +32,8 @@ module UniversalProperty
   (J : Coverage C ℓcov ℓpat)
   where
 
-  -- We assume 'P' to have this level to ensure that 'F' has the same level as 'P'.
+  -- We assume 'P' to have this level to ensure that the sheafification of 'P'
+  -- has the same level as 'P'.
   ℓP = ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓcov ℓpat))
 
   module _
@@ -50,7 +51,7 @@ module UniversalProperty
     open NatTrans
     open Functor
 
-    η : P ⇒ F
+    η : P ⇒ sheafification
     N-ob η c = η⟦⟧
     N-hom η f = funExt (ηNatural f)
 
@@ -62,7 +63,7 @@ module UniversalProperty
 
 {-
            η
-        P --> F
+        P --> sheafification
          \    .
           \   . inducedMap
          α \  .
@@ -72,7 +73,7 @@ module UniversalProperty
 
       private
 
-        ν : {c : ob} → ⟨ F ⟅ c ⟆ ⟩ → ⟨ G ⟅ c ⟆ ⟩
+        ν : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → ⟨ G ⟅ c ⟆ ⟩
 
         ν (trunc x y p q i j) = str (G ⟅ _ ⟆) _ _ (cong ν p) (cong ν q) i j
         ν (restrict f x) = (G ⟪ f ⟫) (ν x)
@@ -109,22 +110,22 @@ module UniversalProperty
             (λ i → ν (fam i)) ,
             λ i j d f g diamond → cong ν (compat i j d f g diamond)
 
-      inducedMap : F ⇒ G
+      inducedMap : sheafification ⇒ G
       N-ob inducedMap c = ν
       N-hom inducedMap f = refl
 
       inducedMapFits : η C^.⋆ inducedMap ≡ α
       inducedMapFits = makeNatTransPath refl
 
       module _
-        (β : F ⇒ G)
+        (β : sheafification ⇒ G)
         (βFits : η C^.⋆ β ≡ α)
         where
 
         open ElimPropAssumptions J P
 
         private
-          B : {c : ob} → ⟨F⟅ c ⟆⟩ → Type _
+          B : {c : ob} → ⟨ sheafification ⟅ c ⟆ ⟩ → Type _
           B x = (β ⟦ _ ⟧) x ≡ ν x
 
           isPropValuedB : isPropValued B
@@ -140,9 +141,9 @@ module UniversalProperty
               (ν x)
               λ patch →
                 let f = patchArr (str (covers _) cover) patch in
-                (G ⟪ f ⟫) ((β ⟦ _ ⟧) x)    ≡⟨ sym (cong (_$ x) (N-hom β f)) ⟩
-                ((β ⟦ _ ⟧) ((F ⟪ f ⟫) x))  ≡⟨ locallyAgree patch ⟩
-                (G ⟪ f ⟫) (ν x)            ∎
+                (G ⟪ f ⟫) ((β ⟦ _ ⟧) x)                 ≡⟨ sym (cong (_$ x) (N-hom β f)) ⟩
+                ((β ⟦ _ ⟧) ((sheafification ⟪ f ⟫) x))  ≡⟨ locallyAgree patch ⟩
+                (G ⟪ f ⟫) (ν x)                         ∎
 
         uniqueness : β ≡ inducedMap
         uniqueness = makeNatTransPath (funExt λ _ → funExt (
@@ -170,7 +171,7 @@ module UniversalProperty
       isUniversal
         (SheafCategory J ℓP ^op)
         ((C^ [ P ,-]) ∘F FullInclusion C^ (isSheaf J))
-        (F , isSheafF)
+        (sheafification , isSheafSheafification)
         η
     sheafificationIsUniversal (G , isSheafG) = record
       { equiv-proof = λ α →