Clean code for category of elements and simplify a presheaf notation

Cubical/Categories/Constructions/Elements.agda

@@ -1,141 +1,103 @@
-
 -- The category of elements of a functor to Set
+module Cubical.Categories.Constructions.Elements where
 
+open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Path
-open import Cubical.Foundations.Prelude
 
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category
-import      Cubical.Categories.Constructions.Slice.Base as Slice
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Isomorphism
-import      Cubical.Categories.Morphism as Morphism
-
 
-module Cubical.Categories.Constructions.Elements where
-
--- some issues
--- * always need to specify objects during composition because can't infer isSet
 open Category
 open Functor
 
 module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
+
+  open Category C
+
+  private
     getIsSet : ∀ {ℓS} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆))
     getIsSet F c = snd (F ⟅ c ⟆)
 
-    Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS)
-    Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
-
-    infix 50 ∫_
-    ∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
-    -- objects are (c , x) pairs where c ∈ C and x ∈ F c
-    (∫ F) .ob = Element F
-    -- morphisms are f : c → c' which take x to x'
-    (∫ F) .Hom[_,_] (c , x) (c' , x')  = fiber (λ (f : C [ c , c' ]) → (F ⟪ f ⟫) x) x'
-    (∫ F) .id {x = (c , x)} = C .id , funExt⁻ (F .F-id) x
-    (∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
-      = (f ⋆⟨ C ⟩ g) , ((F ⟪ f ⋆⟨ C ⟩ g ⟫) x
-                ≡⟨ funExt⁻ (F .F-seq _ _) _ ⟩
-                  (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
-                ≡⟨ cong (F ⟪ g ⟫) p ⟩
-                  (F ⟪ g ⟫) x₁
-                ≡⟨ q ⟩
-                  x₂
-                ∎)
-    (∫ F) .⋆IdL o@{c , x} o1@{c' , x'} f'@(f , p) i
-      = (cIdL i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdL i
-        where
-          isS = getIsSet F c
-          isS' = getIsSet F c'
-          cIdL = C .⋆IdL f
-
-          -- proof from composition with id
-          p' : (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x ≡ x'
-          p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f')
-    (∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
-        = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' ((F ⟪ a ⟫) x) x') p' p cIdR i
-          where
-            cIdR = C .⋆IdR f
-            isS' = getIsSet F c'
-
-            p' : (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x ≡ x'
-            p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id))
-    (∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
-      = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ ((F ⟪ a ⟫) x) x₃) p1 p2 cAssoc i
-        where
-          cAssoc = C .⋆Assoc f g h
-          isS₃ = getIsSet F c₃
-
-          p1 : (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x ≡ x₃
-          p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h')
-
-          p2 : (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x ≡ x₃
-          p2 = snd ((∫ F) ._⋆_ f' ((∫ F) ._⋆_ {o1} {o2} {o3} g' h'))
-    (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
-
-    ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {c,f c',f' : Element F}
-      → {χ1,ef1 χ2,ef2 : (∫ F) [ c,f , c',f' ]} → (fst χ1,ef1 ≡ fst χ2,ef2) → (χ1,ef1 ≡ χ2,ef2)
-    ElementHom≡ F {c1 , f1} {c2 , f2} {χ1 , ef1} {χ2 , ef2} eχ = cong₂ _,_ eχ
-      (fst (isOfHLevelPathP' 0 (snd (F ⟅ c2 ⟆) _ _) ef1 ef2))
-
-    ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
-    F-ob (ForgetElements F) = fst
-    F-hom (ForgetElements F) = fst
-    F-id (ForgetElements F) = refl
-    F-seq (ForgetElements F) _ _ = refl
-
-    module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
-      open isUnivalent
-      isUnivalent∫ : isUnivalent (∫ F)
-      isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
-        ( isoToPath∫
-        , (λ f≅f' → CatIso≡ _ _
-            (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
-              (cong fst
-              (secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
-        , λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
-          ( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
-          ∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
-
-        isoToPath∫ : ∀ {c c' f f'}
-                   → CatIso (∫ F) (c , f) (c' , f')
-                   → (c , f) ≡ (c' , f')
-        isoToPath∫ {f = f} f≅f' = ΣPathP
-          ( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
-          , toPathP ( (λ j → transport (λ i → fst
-                      (F-isoToPath isUnivC isUnivalentSET F
-                        (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
-                    ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
-                    ∙ f≅f' .fst .snd))
-
+  Element : ∀ {ℓS} (F : Functor C (SET ℓS)) → Type (ℓ-max ℓ ℓS)
+  Element F = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
+
+  infix 50 ∫_
+
+  ∫_ : ∀ {ℓS} → Functor C (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
+  -- objects are (c , x) pairs where c ∈ C and x ∈ F c
+  (∫ F) .ob = Element F
+  -- morphisms are f : c → c' which take x to x'
+  (∫ F) .Hom[_,_] (c , x) (c' , x') = fiber (λ (f : C [ c , c' ]) → F .F-hom f x) x'
+  (∫ F) .id     .fst = id C
+  (∫ F) .id {x} .snd = funExt⁻ (F .F-id) (x .snd)
+  (∫ F) ._⋆_ (f , p) (g , q) .fst = f ⋆⟨ C ⟩ g
+  (∫ F) ._⋆_ (f , p) (g , q) .snd = funExt⁻ (F .F-seq _ _) _ ∙∙ cong (F ⟪ g ⟫) p ∙∙ q
+  (∫ F) .⋆IdL _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆IdL C _)
+  (∫ F) .⋆IdR _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆IdR C _)
+  (∫ F) .⋆Assoc _ _ _ = Σ≡Prop (λ _ → getIsSet F _ _ _) (⋆Assoc C _ _ _)
+  (∫ F) .isSetHom {x} {y} = isSetΣSndProp (C .isSetHom) λ _ → (F ⟅ fst y ⟆) .snd _ _
+
+  ElementHom≡ : ∀ {ℓS} (F : Functor C (SET ℓS)) → {x y : Element F}
+              → {f g : (∫ F) [ x , y ]} → fst f ≡ fst g → f ≡ g
+  ElementHom≡ F = Σ≡Prop (λ _ → getIsSet F _ _ _)
+
+  ForgetElements : ∀ {ℓS} → (F : Functor C (SET ℓS)) → Functor (∫ F) C
+  F-ob (ForgetElements F) = fst
+  F-hom (ForgetElements F) = fst
+  F-id (ForgetElements F) = refl
+  F-seq (ForgetElements F) _ _ = refl
+
+  module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
+    open isUnivalent
+    isUnivalent∫ : isUnivalent (∫ F)
+    isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
+      ( isoToPath∫
+      , (λ f≅f' → CatIso≡ _ _
+          (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
+            (cong fst
+            (secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
+      , λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
+        ( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
+        ∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
+
+      isoToPath∫ : ∀ {c c' f f'}
+                 → CatIso (∫ F) (c , f) (c' , f')
+                 → (c , f) ≡ (c' , f')
+      isoToPath∫ {f = f} f≅f' = ΣPathP
+        ( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
+        , toPathP ( (λ j → transport (λ i → fst
+                    (F-isoToPath isUnivC isUnivalentSET F
+                      (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
+                  ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
+                  ∙ f≅f' .fst .snd))
 
 module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
-    open Covariant {C = C ^op}
+  open Covariant {C = C ^op}
 
-    -- same thing but for presheaves
-    ∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
-    ∫ᴾ F = (∫ F) ^op
+  -- same thing but for presheaves
+  ∫ᴾ_ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Category (ℓ-max ℓ ℓS) (ℓ-max ℓ' ℓS)
+  ∫ᴾ F = (∫ F) ^op
 
-    Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS)
-    Elementᴾ F = (∫ᴾ F) .ob
+  Elementᴾ : ∀ {ℓS} → Functor (C ^op) (SET ℓS) → Type (ℓ-max ℓ ℓS)
+  Elementᴾ F = (∫ᴾ F) .ob
 
-    -- helpful results
+  -- helpful results
 
-    module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where
+  module _ {ℓS} {F : Functor (C ^op) (SET ℓS)} where
 
-      -- morphisms are equal as long as the morphisms in C are equal
-      ∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ])
-              → (p : o1 ≡ o1') (q : o2 ≡ o2')
-              → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
-              → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
-      ∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _)
+    -- morphisms are equal as long as the morphisms in C are equal
+    ∫ᴾhomEq : ∀ {o1 o1' o2 o2'} (f : (∫ᴾ F) [ o1 , o2 ]) (g : (∫ᴾ F) [ o1' , o2' ])
+            → (p : o1 ≡ o1') (q : o2 ≡ o2')
+            → (eqInC : PathP (λ i → C [ fst (p i) , fst (q i) ]) (fst f) (fst g))
+            → PathP (λ i → (∫ᴾ F) [ p i , q i ]) f g
+    ∫ᴾhomEq _ _ _ _ = ΣPathPProp (λ f → snd (F ⟅ _ ⟆) _ _)
 
-      ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ])
-                   → fst f ≡ fst g → f ≡ g
-      ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p
+    ∫ᴾhomEqSimpl : ∀ {o1 o2} (f g : (∫ᴾ F) [ o1 , o2 ])
+                 → fst f ≡ fst g → f ≡ g
+    ∫ᴾhomEqSimpl f g p = ∫ᴾhomEq f g refl refl p

Cubical/Categories/Presheaf/Base.agda

@@ -26,21 +26,21 @@ isUnivalentPresheafCategory = isUnivalentFUNCTOR _ _ isUnivalentSET
 open Category
 open Functor
 
-action : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS)
+action : {C : Category ℓ ℓ'} → (P : Presheaf C ℓS)
        → {a b : C .ob} → C [ a , b ] → fst (P ⟅ b ⟆) → fst (P ⟅ a ⟆)
-action C P = P .F-hom
+action P = P .F-hom
 
 -- Convenient notation for naturality
-syntax action C P f ϕ = ϕ ∘ᴾ⟨ C , P ⟩ f
+syntax action P f ϕ = ϕ ∘ᴾ⟨ P ⟩ f
 
 ∘ᴾId : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a : C .ob}
      → (ϕ : fst (P ⟅ a ⟆))
-     → ϕ ∘ᴾ⟨ C , P ⟩ C .id ≡ ϕ
+     → ϕ ∘ᴾ⟨ P ⟩ C .id ≡ ϕ
 ∘ᴾId C P ϕ i = P .F-id i ϕ
 
 ∘ᴾAssoc : ∀ (C : Category ℓ ℓ') → (P : Presheaf C ℓS) → {a b c : C .ob}
         → (ϕ : fst (P ⟅ c ⟆))
         → (f : C [ b , c ])
         → (g : C [ a , b ])
-        → ϕ ∘ᴾ⟨ C , P ⟩ (f ∘⟨ C ⟩ g) ≡ (ϕ ∘ᴾ⟨ C , P ⟩ f) ∘ᴾ⟨ C , P ⟩ g
+        → ϕ ∘ᴾ⟨ P ⟩ (f ∘⟨ C ⟩ g) ≡ (ϕ ∘ᴾ⟨ P ⟩ f) ∘ᴾ⟨ P ⟩ g
 ∘ᴾAssoc C P ϕ f g i = P .F-seq f g i ϕ

Cubical/Categories/Presheaf/Morphism.agda

@@ -56,17 +56,17 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
     pushElt (A , η) = (F ⟅ A ⟆) , (h .N-ob A (lift η) .lower)
 
     pushEltNat : ∀ {B : C .ob} (η : Elementᴾ {C = C} P) (f : C [ B , η .fst ])
-                  → (pushElt η .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f)
-                    ≡ pushElt (B , η .snd ∘ᴾ⟨ C , P ⟩ f) .snd
+                  → (pushElt η .snd ∘ᴾ⟨ Q ⟩ F .F-hom f)
+                    ≡ pushElt (B , η .snd ∘ᴾ⟨ P ⟩ f) .snd
     pushEltNat η f i = h .N-hom f (~ i) (lift (η .snd)) .lower
 
     pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q)
     pushEltF .F-ob = pushElt
     pushEltF .F-hom {x}{y} (f , commutes) .fst = F .F-hom f
     pushEltF .F-hom {x}{y} (f , commutes) .snd =
-      pushElt _ .snd ∘ᴾ⟨ D , Q ⟩ F .F-hom f
+      pushElt _ .snd ∘ᴾ⟨ Q ⟩ F .F-hom f
         ≡⟨ pushEltNat y f ⟩
-      pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd
+      pushElt (_ , y .snd ∘ᴾ⟨ P ⟩ f) .snd
         ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , commutes)) ⟩
       pushElt x .snd ∎
     pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id)

Cubical/Categories/Presheaf/Representable.agda

@@ -74,7 +74,7 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
   isUniversal : (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst)
               → Type (ℓ-max (ℓ-max ℓo ℓh) ℓp)
   isUniversal vertex element =
-    ∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ C , P ⟩ f
+    ∀ A → isEquiv λ (f : C [ A , vertex ]) → element ∘ᴾ⟨ P ⟩ f
 
   isPropIsUniversal : ∀ vertex element → isProp (isUniversal vertex element)
   isPropIsUniversal vertex element = isPropΠ (λ _ → isPropIsEquiv _)