Improve definitional behavior of the category of elements

Align with the definition of a fiber to simplify arguments down the line.

Cubical/Categories/Constructions/Elements.agda

@@ -2,26 +2,32 @@
 
 -- The Category of Elements
 
-open import Cubical.Categories.Category
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Prelude
 
-module Cubical.Categories.Constructions.Elements where
+open import Cubical.Data.Sigma
 
-open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Category
+import      Cubical.Categories.Constructions.Slice.Base as Slice
 open import Cubical.Categories.Functor
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Data.Sigma
+open import Cubical.Categories.Instances.Sets
+open import Cubical.Categories.Isomorphism
+import      Cubical.Categories.Morphism as Morphism
+
 
-import Cubical.Categories.Morphism as Morphism
-import Cubical.Categories.Constructions.Slice.Base as Slice
+
+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
-    getIsSet : ∀ {ℓS} {C : Category ℓ ℓ'} (F : Functor C (SET ℓS)) → (c : C .ob) → isSet (fst (F ⟅ c ⟆))
+    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)
@@ -32,45 +38,45 @@ module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     -- 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')  = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x
-    (∫ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
+    (∫ 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) , (x₂
-                ≡⟨ q ⟩
-                  (F ⟪ g ⟫) x₁         -- basically expanding out function composition
-                ≡⟨ cong (F ⟪ g ⟫) p ⟩
+      = (f ⋆⟨ C ⟩ g) , ((F ⟪ f ⋆⟨ C ⟩ g ⟫) x
+                ≡⟨ funExt⁻ (F .F-seq _ _) _ ⟩
                   (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
-                ≡⟨ funExt⁻ (sym (F .F-seq _ _)) _ ⟩
-                  (F ⟪ f ⋆⟨ C ⟩ g ⟫) 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' x' ((F ⟪ a ⟫) x)) p' p cIdL 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' : x' ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x
+          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' x' ((F ⟪ a ⟫) x)) p' p cIdR 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' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x
+            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₃ x₃ ((F ⟪ a ⟫) x)) p1 p2 cAssoc 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 : x₃ ≡ (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x
+          p1 : (F ⟪ (f ⋆⟨ C ⟩ g) ⋆⟨ C ⟩ h ⟫) x ≡ x₃
           p1 = snd ((∫ F) ._⋆_ ((∫ F) ._⋆_ {o} {o1} {o2} f' g') h')
 
-          p2 : x₃ ≡ (F ⟪ f ⋆⟨ C ⟩ (g ⋆⟨ C ⟩ h) ⟫) x
+          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 _ _
 

Cubical/Categories/Constructions/Slice/Properties.agda

@@ -31,13 +31,13 @@ open WeakInverse
 
 slice→el : Functor (SliceCat C c) (∫ᴾ (C [-, c ]))
 slice→el .F-ob s = s .S-ob , s .S-arr
-slice→el .F-hom f = f .S-hom , sym (f .S-comm)
+slice→el .F-hom f = f .S-hom , f .S-comm
 slice→el .F-id = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _))
 slice→el .F-seq _ _ = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _))
 
 el→slice : Functor (∫ᴾ (C [-, c ])) (SliceCat C c)
 el→slice .F-ob (_ , s) = sliceob s
-el→slice .F-hom (f , comm) = slicehom f (sym comm)
+el→slice .F-hom (f , comm) = slicehom f comm
 el→slice .F-id = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)
 el→slice .F-seq _ _ = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)
 

Cubical/Categories/Presheaf/Morphism.agda

@@ -63,12 +63,13 @@ module _ {C : Category ℓc ℓc'}{D : Category ℓd ℓd'}
 
     pushEltF : Functor (∫ᴾ_ {C = C} P) (∫ᴾ_ {C = D} Q)
     pushEltF .F-ob = pushElt
-    pushEltF .F-hom {x}{y} (f , commutes) = F .F-hom f , sym (
+    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
         ≡⟨ pushEltNat y f ⟩
       pushElt (_ , y .snd ∘ᴾ⟨ C , P ⟩ f) .snd
-        ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , (sym commutes))) ⟩
-      pushElt x .snd ∎)
+        ≡⟨ cong (λ a → pushElt a .snd) (ΣPathP (refl , commutes)) ⟩
+      pushElt x .snd ∎
     pushEltF .F-id = Σ≡Prop (λ x → (Q ⟅ _ ⟆) .snd _ _) (F .F-id)
     pushEltF .F-seq f g =
       Σ≡Prop ((λ x → (Q ⟅ _ ⟆) .snd _ _)) (F .F-seq (f .fst) (g .fst))

Cubical/Categories/Presheaf/Properties.agda

@@ -68,7 +68,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
       (F ⟪ h ⟫) ((ϕ ⟦ d ⟧) b)
     ≡[ i ]⟨ (F ⟪ h ⟫) (eq i) ⟩
       (F ⟪ h ⟫) y
-    ≡⟨ sym com ⟩
+    ≡⟨ com ⟩
       x
     ∎)
   -- functoriality follows from functoriality of A
@@ -153,7 +153,7 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
                 rightEq = left ▷ right
                   where
                     -- the id morphism in (∫ᴾ F)
-                    ∫id = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
+                    ∫id = C .id , funExt⁻ (F .F-id) x
 
                     -- functoriality of P gives us close to what we want
                     right : (P ⟪ ∫id ⟫) X ≡ X
@@ -326,8 +326,8 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
               right : PathP (λ i → fst (P ⟅ d , eq' i ⟆)) ((P ⟪ f , refl ⟫) X') ((P ⟪ f , comm ⟫) (subst _ eq X'))
               right i = (P ⟪ f , refl≡comm i ⟫) (X'≡subst i)
                 where
-                  refl≡comm : PathP (λ i → (eq' i) ≡ (F ⟪ f ⟫) (eq i)) refl comm
-                  refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) v ((F ⟪ f ⟫) w)) refl comm λ i → (eq' i , eq i)
+                  refl≡comm : PathP (λ i → (F ⟪ f ⟫) (eq i) ≡ (eq' i)) refl comm
+                  refl≡comm = isOfHLevel→isOfHLevelDep 1 (λ (v , w) → snd (F ⟅ d ⟆) ((F ⟪ f ⟫) w) v) refl comm λ i → (eq' i , eq i)
 
                   X'≡subst : PathP (λ i → fst (P ⟅ c , eq i ⟆)) X' (subst _ eq X')
                   X'≡subst = transport-filler (λ i → fst (P ⟅ c , eq i ⟆)) X'

Cubical/Categories/Presheaf/Representable.agda

@@ -150,10 +150,10 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
   isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .fst =
     term (_ , ϕ) .fst .fst
   isTerminalToIsUniversal {η} term A .equiv-proof ϕ .fst .snd =
-    sym (term (_ , ϕ) .fst .snd)
+    term (_ , ϕ) .fst .snd
   isTerminalToIsUniversal {η} term A .equiv-proof ϕ .snd (f , commutes) =
     Σ≡Prop (λ _ → (P ⟅ A ⟆) .snd _ _)
-           (cong fst (term (A , ϕ) .snd (f , sym commutes)))
+           (cong fst (term (A , ϕ) .snd (f , commutes)))
 
   isUniversalToIsTerminal :
     ∀ (vertex : C .ob) (element : (P ⟅ vertex ⟆) .fst)
@@ -162,11 +162,11 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where
   isUniversalToIsTerminal vertex element universal ϕ .fst .fst =
     universal _ .equiv-proof (ϕ .snd) .fst .fst
   isUniversalToIsTerminal vertex element universal ϕ .fst .snd =
-    sym (universal _ .equiv-proof (ϕ .snd) .fst .snd)
+    universal _ .equiv-proof (ϕ .snd) .fst .snd
   isUniversalToIsTerminal vertex element universal ϕ .snd (f , commutes) =
     Σ≡Prop
       (λ _ → (P ⟅ _ ⟆) .snd _ _)
-      (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , sym commutes)))
+      (cong fst (universal _ .equiv-proof (ϕ .snd) .snd (f , commutes)))
 
   terminalElementToUniversalElement : TerminalElement → UniversalElement
   terminalElementToUniversalElement η .vertex = η .fst .fst