Make the category C explicit (#634)

* Make the category `C` explicit

In `Categories/Morphism.agda`:
- `isMonic`
- `isEpic`
- `isSplitMon`
- `isSplitEpi`
- `areInv`
- `isIso`

In `Categories/Category/Base.agda`: `CatIso`

* Fix whitespace

Cubical/Categories/Category/Base.agda

@@ -48,16 +48,16 @@ infixr 16 comp'
 syntax comp' C g f = g ∘⟨ C ⟩ f
 
 -- Isomorphisms and paths in categories
-record CatIso {C : Category ℓ ℓ'} (x y : C .ob) : Type ℓ' where
+record CatIso (C : Category ℓ ℓ') (x y : C .ob) : Type ℓ' where
   constructor catiso
   field
     mor : C [ x , y ]
     inv : C [ y , x ]
     sec : inv ⋆⟨ C ⟩ mor ≡ C .id
     ret : mor ⋆⟨ C ⟩ inv ≡ C .id
 
-pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso {C = C} x y
-pathToIso {C = C} p = J (λ z _ → CatIso _ z) (catiso idx idx (C .⋆IdL idx) (C .⋆IdL idx)) p
+pathToIso : {C : Category ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso C x y
+pathToIso {C = C} p = J (λ z _ → CatIso _ _ z) (catiso idx idx (C .⋆IdL idx) (C .⋆IdL idx)) p
   where
     idx = C .id
 
@@ -67,11 +67,11 @@ record isUnivalent (C : Category ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
     univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y})
 
   -- package up the univalence equivalence
-  univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso x y)
+  univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso _ x y)
   univEquiv x y = pathToIso , univ x y
 
   -- The function extracting paths from category-theoretic isomorphisms.
-  CatIsoToPath : {x y : C .ob} (p : CatIso x y) → x ≡ y
+  CatIsoToPath : {x y : C .ob} (p : CatIso _ x y) → x ≡ y
   CatIsoToPath {x = x} {y = y} p =
     equivFun (invEquiv (univEquiv x y)) p
 

Cubical/Categories/Constructions/Slice.agda

@@ -158,18 +158,18 @@ module _ ⦃ isU : isUnivalent C ⦄ where
 
     -- names for the equivalences/isos
 
-    pathIsoEquiv : (x ≡ y) ≃ (CatIso x y)
+    pathIsoEquiv : (x ≡ y) ≃ (CatIso _ x y)
     pathIsoEquiv = univEquiv isU x y
 
-    isoPathEquiv : (CatIso x y) ≃ (x ≡ y)
+    isoPathEquiv : (CatIso _ x y) ≃ (x ≡ y)
     isoPathEquiv = invEquiv pathIsoEquiv
 
-    pToIIso' : Iso (x ≡ y) (CatIso x y)
+    pToIIso' : Iso (x ≡ y) (CatIso _ x y)
     pToIIso' = equivToIso pathIsoEquiv
 
     -- the iso in SliceCat we're given induces an iso in C between x and y
-    module _ ( cIso@(catiso kc lc s r) : CatIso {C = SliceCat} xf yg ) where
-      extractIso' : CatIso {C = C} x y
+    module _ ( cIso@(catiso kc lc s r) : CatIso SliceCat xf yg ) where
+      extractIso' : CatIso C x y
       extractIso' .mor = kc .S-hom
       extractIso' .inv = lc .S-hom
       extractIso' .sec i = (s i) .S-hom
@@ -181,11 +181,11 @@ module _ ⦃ isU : isUnivalent C ⦄ where
     preservesUnivalenceSlice .univ xf@(sliceob {x} f) yg@(sliceob {y} g) = isoToIsEquiv sIso
       where
         -- this is just here because the type checker can't seem to infer xf and yg
-        pToIIso : Iso (x ≡ y) (CatIso x y)
+        pToIIso : Iso (x ≡ y) (CatIso _ x y)
         pToIIso = pToIIso' {xf = xf} {yg}
 
         -- the meat of the proof
-        sIso : Iso (xf ≡ yg) (CatIso xf yg)
+        sIso : Iso (xf ≡ yg) (CatIso _ xf yg)
         sIso .fun p = pathToIso p -- we use the normal pathToIso via path induction to get an isomorphism
         sIso .inv is@(catiso kc lc s r) = SliceOb-≡-intro x≡y (symP (sym (lc .S-comm) ◁ lf≡f))
           where
@@ -201,7 +201,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where
             l = lc .S-hom
 
             -- extract out the iso between x and y
-            extractIso : CatIso {C = C} x y
+            extractIso : CatIso C x y
             extractIso = extractIso' is
 
             -- and we can use univalence of C to get x ≡ y
@@ -216,7 +216,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where
                         x≡y
               where
                 idx = C .id
-                pToIFam = (λ z _ → CatIso {C = C} x z)
+                pToIFam = (λ z _ → CatIso C x z)
                 pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)
 
             l≡pToI : l ≡ pathToIso {C = C} x≡y .inv
@@ -238,7 +238,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where
             k = kc .S-hom
             l = lc .S-hom
 
-            extractIso : CatIso {C = C} x y
+            extractIso : CatIso C x y
             extractIso = extractIso' is
 
             -- we do the equality component wise
@@ -305,11 +305,11 @@ module _ ⦃ isU : isUnivalent C ⦄ where
                            p
                where
                  idx = C .id
-                 pToIFam = (λ z _ → CatIso {C = C} x z)
+                 pToIFam = (λ z _ → CatIso C x z)
                  pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)
 
                  idxf = SliceCat .id
-                 pToIFam' = (λ z _ → CatIso {C = SliceCat} xf z)
+                 pToIFam' = (λ z _ → CatIso SliceCat xf z)
                  pToIBase' = catiso (SliceCat .id) idxf (SliceCat .⋆IdL idxf) (SliceCat .⋆IdL idxf)
 
             -- why does this not follow definitionally?
@@ -370,8 +370,8 @@ open isIsoC renaming (inv to invC)
 
 -- make a slice isomorphism from just the hom
 sliceIso : ∀ {a b} (f : C [ a .S-ob , b .S-ob ]) (c : (f ⋆⟨ C ⟩ b .S-arr) ≡ a .S-arr)
-         → isIsoC {C = C} f
-         → isIsoC {C = SliceCat} (slicehom f c)
+         → isIsoC C f
+         → isIsoC SliceCat (slicehom f c)
 sliceIso f c isof .invC = slicehom (isof .invC) (sym (invMoveL (isIso→areInv isof) c))
 sliceIso f c isof .sec = SliceHom-≡-intro' (isof .sec)
 sliceIso f c isof .ret = SliceHom-≡-intro' (isof .ret)

Cubical/Categories/Equivalence/Properties.agda

@@ -71,10 +71,10 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
       Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor
       Gg≡ηhη = invMoveL cAreInv move-c' ∙ sym (C .⋆Assoc _ _ _)
         where
-          cAreInv : areInv (cIso .mor) (cIso .inv)
+          cAreInv : areInv _ (cIso .mor) (cIso .inv)
           cAreInv = CatIso→areInv cIso
 
-          c'AreInv : areInv (c'Iso .mor) (c'Iso .inv)
+          c'AreInv : areInv _ (c'Iso .mor) (c'Iso .inv)
           c'AreInv = CatIso→areInv c'Iso
 
           move-c' : cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .mor

Cubical/Categories/Functor/Base.agda

@@ -26,7 +26,7 @@ record Functor (C : Category ℓC ℓC') (D : Category ℓD ℓD') :
 
   isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f]
   isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g
-  isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso {C = D} (F-ob c) d
+  isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso D (F-ob c) d
 
 private
   variable

Cubical/Categories/Functor/Properties.agda

@@ -81,7 +81,7 @@ module _ {F : Functor C D} where
     ∎
 
   -- functors preserve isomorphisms
-  preserveIsosF : ∀ {x y} → CatIso {C = C} x y → CatIso {C = D} (F ⟅ x ⟆) (F ⟅ y ⟆)
+  preserveIsosF : ∀ {x y} → CatIso C x y → CatIso D (F ⟅ x ⟆) (F ⟅ y ⟆)
   preserveIsosF {x} {y} (catiso f f⁻¹ sec' ret') =
     catiso
       g g⁻¹

Cubical/Categories/Instances/Functors.agda

@@ -31,8 +31,8 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
   open isIsoC renaming (inv to invC)
   -- componentwise iso is an iso in Functor
   FUNCTORIso : ∀ {F G : Functor C D} (α : F ⇒ G)
-             → (∀ (c : C .ob) → isIsoC {C = D} (α ⟦ c ⟧))
-             → isIsoC {C = FUNCTOR} α
+             → (∀ (c : C .ob) → isIsoC D (α ⟦ c ⟧))
+             → isIsoC FUNCTOR α
   FUNCTORIso α is .invC .N-ob c = (is c) .invC
   FUNCTORIso {F} {G} α is .invC .N-hom {c} {d} f
     = invMoveL areInv-αc
@@ -43,10 +43,10 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
                  F ⟪ f ⟫
                ∎ )
     where
-      areInv-αc : areInv (α ⟦ c ⟧) ((is c) .invC)
+      areInv-αc : areInv _ (α ⟦ c ⟧) ((is c) .invC)
       areInv-αc = isIso→areInv (is c)
 
-      areInv-αd : areInv (α ⟦ d ⟧) ((is d) .invC)
+      areInv-αd : areInv _ (α ⟦ d ⟧) ((is d) .invC)
       areInv-αd = isIso→areInv (is d)
   FUNCTORIso α is .sec = makeNatTransPath (funExt (λ c → (is c) .sec))
   FUNCTORIso α is .ret = makeNatTransPath (funExt (λ c → (is c) .ret))

Cubical/Categories/Instances/Sets.agda

@@ -65,7 +65,7 @@ open Iso
 
 Iso→CatIso : ∀ {A B : (SET ℓ) .ob}
            → Iso (fst A) (fst B)
-           → CatIso {C = SET ℓ} A B
+           → CatIso (SET ℓ) A B
 Iso→CatIso is .mor = is .fun
 Iso→CatIso is .cInv = is .inv
 Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv

Cubical/Categories/Limits/Terminal.agda

@@ -34,7 +34,7 @@ module _ (C : Category ℓ ℓ') where
 
   -- Objects that are initial are isomorphic.
   isInitialToIso : {x y : ob} (hx : isInitial x) (hy : isInitial y) →
-    CatIso {C = C} x y
+    CatIso C x y
   isInitialToIso {x = x} {y = y} hx hy =
     let x→y : C [ x , y ]
         x→y = fst (hx y) -- morphism forwards
@@ -65,7 +65,7 @@ module _ (C : Category ℓ ℓ') where
 
   -- Objects that are initial are isomorphic.
   isFinalToIso : {x y : ob} (hx : isFinal x) (hy : isFinal y) →
-    CatIso {C = C} x y
+    CatIso C x y
   isFinalToIso {x = x} {y = y} hx hy =
     let x→y : C [ x , y ]
         x→y = fst (hy x) -- morphism forwards

Cubical/Categories/Morphism.agda

@@ -2,16 +2,16 @@
 module Cubical.Categories.Morphism where
 
 open import Cubical.Foundations.Prelude
-
 open import Cubical.Data.Sigma
-
 open import Cubical.Categories.Category
 
+
 private
   variable
     ℓ ℓ' : Level
 
-module _ {C : Category ℓ ℓ'} where
+-- C needs to be explicit for these definitions as Agda can't infer it
+module _ (C : Category ℓ ℓ') where
   open Category C
 
   private
@@ -39,15 +39,30 @@ module _ {C : Category ℓ ℓ'} where
       sec : g ⋆ f ≡ id
       ret : f ⋆ g ≡ id
 
+  record isIso (f : Hom[ x , y ]) : Type ℓ' where
+    field
+      inv : Hom[ y , x ]
+      sec : inv ⋆ f ≡ id
+      ret : f ⋆ inv ≡ id
+
+
+-- C can be implicit here
+module _ {C : Category ℓ ℓ'} where
+  open Category C
+
+  private
+    variable
+      x y z w : ob
+
   open areInv
 
-  symAreInv : {f : Hom[ x , y ]} {g : Hom[ y , x ]} → areInv f g → areInv g f
+  symAreInv : {f : Hom[ x , y ]} {g : Hom[ y , x ]} → areInv C f g → areInv C g f
   sec (symAreInv x) = ret x
   ret (symAreInv x) = sec x
 
   -- equational reasoning with inverses
   invMoveR : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ z , x ]} {k : Hom[ z , y ]}
-           → areInv f g
+           → areInv C f g
            → h ⋆ f ≡ k
            → h ≡ k ⋆ g
   invMoveR {f = f} {g} {h} {k} ai p
@@ -63,7 +78,7 @@ module _ {C : Category ℓ ℓ'} where
     ∎
 
   invMoveL : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ y , z ]} {k : Hom[ x , z ]}
-          → areInv f g
+          → areInv C f g
           → f ⋆ h ≡ k
           → h ≡ g ⋆ k
   invMoveL {f = f} {g} {h} {k} ai p
@@ -78,43 +93,37 @@ module _ {C : Category ℓ ℓ'} where
       (g ⋆ k)
     ∎
 
-  record isIso (f : Hom[ x , y ]) : Type ℓ' where
-    field
-      inv : Hom[ y , x ]
-      sec : inv ⋆ f ≡ id
-      ret : f ⋆ inv ≡ id
-
   open isIso
 
   isIso→areInv : ∀ {f : Hom[ x , y ]}
-               → (isI : isIso f)
-               → areInv f (isI .inv)
+               → (isI : isIso C f)
+               → areInv C f (isI .inv)
   sec (isIso→areInv isI) = sec isI
   ret (isIso→areInv isI) = ret isI
 
   open CatIso
 
   -- isIso agrees with CatIso
   isIso→CatIso : ∀ {f : C [ x , y ]}
-               → isIso f
-               → CatIso {C = C} x y
+               → isIso C f
+               → CatIso C x y
   mor (isIso→CatIso {f = f} x) = f
   inv (isIso→CatIso x) = inv x
   sec (isIso→CatIso x) = sec x
   ret (isIso→CatIso x) = ret x
 
-  CatIso→isIso : (cIso : CatIso {C = C} x y)
-               → isIso (cIso .mor)
+  CatIso→isIso : (cIso : CatIso C x y)
+               → isIso C (cIso .mor)
   inv (CatIso→isIso f) = inv f
   sec (CatIso→isIso f) = sec f
   ret (CatIso→isIso f) = ret f
 
-  CatIso→areInv : (cIso : CatIso {C = C} x y)
-                → areInv (cIso .mor) (cIso .inv)
+  CatIso→areInv : (cIso : CatIso C x y)
+                → areInv C (cIso .mor) (cIso .inv)
   CatIso→areInv cIso = isIso→areInv (CatIso→isIso cIso)
 
   -- reverse of an iso is also an iso
   symCatIso : ∀ {x y}
-             → CatIso {C = C} x y
-             → CatIso {C = C} y x
+             → CatIso C x y
+             → CatIso C y x
   symCatIso (catiso mor inv sec ret) = catiso inv mor ret sec

Cubical/Categories/NaturalTransformation/Base.agda

@@ -47,7 +47,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
     open NatTrans trans
 
     field
-      nIso : ∀ (x : C .ob) → isIsoC {C = D} (N-ob x)
+      nIso : ∀ (x : C .ob) → isIsoC D (N-ob x)
 
     open isIsoC
 

Cubical/Categories/Presheaf.agda

@@ -3,6 +3,5 @@
 module Cubical.Categories.Presheaf where
 
 open import Cubical.Categories.Presheaf.Base public
-open import Cubical.Categories.Presheaf.Properties public
-
 open import Cubical.Categories.Presheaf.KanExtension public
+open import Cubical.Categories.Presheaf.Properties public

Cubical/Categories/Presheaf/Properties.agda

@@ -272,11 +272,11 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
 
     -- isomorphism follows from typeSectionIso
     ηIso : ∀ (sob : SliceCat .ob)
-          → isIsoC {C = SliceCat} (ηTrans ⟦ sob ⟧)
+          → isIsoC SliceCat (ηTrans ⟦ sob ⟧)
     ηIso sob@(sliceob ϕ) = sliceIso _ _ (FUNCTORIso _ _ _ isIsoCf)
       where
         isIsoCf : ∀ (c : C .ob)
-                → isIsoC (ηTrans .N-ob sob .S-hom ⟦ c ⟧)
+                → isIsoC _ (ηTrans .N-ob sob .S-hom ⟦ c ⟧)
         isIsoCf c = CatIso→isIso (Iso→CatIso (typeSectionIso {isSetB = snd (F ⟅ c ⟆)} (ϕ ⟦ c ⟧)))
 
 
@@ -370,11 +370,11 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS))
                 eq'≡eq = snd (F ⟅ c ⟆) _ _ eq' eq
 
     εIso : ∀ (P : PreShv (∫ᴾ F) ℓS .ob)
-          → isIsoC {C = PreShv (∫ᴾ F) ℓS} (εTrans ⟦ P ⟧)
+          → isIsoC (PreShv (∫ᴾ F) ℓS) (εTrans ⟦ P ⟧)
     εIso P = FUNCTORIso _ _ _ isIsoC'
       where
         isIsoC' : ∀ (cx : (∫ᴾ F) .ob)
-                → isIsoC {C = SET _} ((εTrans ⟦ P ⟧) ⟦ cx ⟧)
+                → isIsoC (SET _) ((εTrans ⟦ P ⟧) ⟦ cx ⟧)
         isIsoC' cx@(c , _) = CatIso→isIso (Iso→CatIso (invIso (typeFiberIso {isSetA = snd (F ⟅ c ⟆)} _)))