Rename arrowIsSet to arrowsAreSets

src/Cat/Categories/Cat.agda

@@ -88,7 +88,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
       module D = Category 𝔻
       open import Cubical.Sigma
       issSet : {A B : RawCategory.Object :rawProduct:} → isSet (Arrow A B)
-      issSet = setSig {sA = C.arrowIsSet} {sB = λ x → D.arrowIsSet}
+      issSet = setSig {sA = C.arrowsAreSets} {sB = λ x → D.arrowsAreSets}
       ident' : IsIdentity :𝟙:
       ident'
         = Σ≡ (fst C.isIdentity) (fst D.isIdentity)
@@ -98,7 +98,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
         :isCategory: : IsCategory :rawProduct:
         IsCategory.isAssociative :isCategory: = Σ≡ C.isAssociative D.isAssociative
         IsCategory.isIdentity :isCategory: = ident'
-        IsCategory.arrowIsSet :isCategory: = issSet
+        IsCategory.arrowsAreSets :isCategory: = issSet
         IsCategory.univalent :isCategory: = univalent
 
       :product: : Category ℓ ℓ'

src/Cat/Categories/Fam.agda

@@ -46,7 +46,7 @@ module _ (ℓa ℓb : Level) where
       isCategory = record
         { isAssociative = λ {A} {B} {C} {D} {f} {g} {h} → isAssociative {D = D} {f} {g} {h}
         ; isIdentity = λ {A} {B} {f} → isIdentity {A} {B} {f = f}
-        ; arrowIsSet = {!!}
+        ; arrowsAreSets = {!!}
         ; univalent = {!!}
         }
 

src/Cat/Categories/Free.agda

@@ -59,6 +59,6 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   RawIsCategoryFree = record
     { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}}
     ; isIdentity = ident-r , ident-l
-    ; arrowIsSet = {!!}
+    ; arrowsAreSets = {!!}
     ; univalent = {!!}
     }

src/Cat/Categories/Fun.agda

@@ -101,13 +101,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
 
   module _ {F G : Functor ℂ 𝔻} where
     transformationIsSet : isSet (Transformation F G)
-    transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
+    transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C)   (λ l → q l C) i j
 
     naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
     naturalIsProp θ θNat θNat' = lem
       where
         lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
-        lem = λ i f → 𝔻.arrowIsSet _ _ (θNat f) (θNat' f) i
+        lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
 
     naturalTransformationIsSets : isSet (NaturalTransformation F G)
     naturalTransformationIsSets = sigPresSet transformationIsSet
@@ -170,7 +170,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     :isCategory: = record
       { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D}
       ; isIdentity = λ {A B} → :ident: {A} {B}
-      ; arrowIsSet = λ {F} {G} → naturalTransformationIsSets {F} {G}
+      ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G}
       ; univalent = {!!}
       }
 

src/Cat/Categories/Rel.agda

@@ -166,6 +166,6 @@ RawIsCategoryRel : IsCategory RawRel
 RawIsCategoryRel = record
   { isAssociative = funExt is-isAssociative
   ; isIdentity = funExt ident-l , funExt ident-r
-  ; arrowIsSet = {!!}
+  ; arrowsAreSets = {!!}
   ; univalent = {!!}
   }

src/Cat/Categories/Sets.agda

@@ -28,7 +28,7 @@ module _ (ℓ : Level) where
     isAssociative SetsIsCategory = refl
     proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
     proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
-    arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
+    arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
     univalent SetsIsCategory = {!!}
 
   𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
@@ -94,7 +94,7 @@ module _ {ℓa ℓb : Level} where
   representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
   representable {ℂ = ℂ} A = record
     { raw = record
-      { func* = λ B → ℂ [ A , B ] , arrowIsSet
+      { func* = λ B → ℂ [ A , B ] , arrowsAreSets
       ; func→ = ℂ [_∘_]
       }
     ; isFunctor = record
@@ -109,7 +109,7 @@ module _ {ℓa ℓb : Level} where
   presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
   presheaf {ℂ = ℂ} B = record
     { raw = record
-      { func* = λ A → ℂ [ A , B ] , arrowIsSet
+      { func* = λ A → ℂ [ A , B ] , arrowsAreSets
       ; func→ = λ f g → ℂ [ g ∘ f ]
     }
     ; isFunctor = record

src/Cat/Category.agda

@@ -103,7 +103,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   field
     isAssociative : IsAssociative
     isIdentity : IsIdentity 𝟙
-    arrowIsSet : ArrowsAreSets
+    arrowsAreSets : ArrowsAreSets
     univalent : Univalent isIdentity
 
 -- `IsCategory` is a mere proposition.
@@ -115,12 +115,12 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     open import Cubical.NType.Properties
 
     propIsAssociative : isProp IsAssociative
-    propIsAssociative x y i = arrowIsSet _ _ x y i
+    propIsAssociative x y i = arrowsAreSets _ _ x y i
 
     propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
     propIsIdentity a b i
-      = arrowIsSet _ _ (fst a) (fst b) i
+      = arrowsAreSets _ _ (fst a) (fst b) i
-      , arrowIsSet _ _ (snd a) (snd b) i
+      , arrowsAreSets _ _ (snd a) (snd b) i
 
     propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
     propArrowIsSet a b i = isSetIsProp a b i
@@ -129,9 +129,9 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
     propIsInverseOf x y = λ i →
       let
         h : fst x ≡ fst y
-        h = arrowIsSet _ _ (fst x) (fst y)
+        h = arrowsAreSets _ _ (fst x) (fst y)
         hh : snd x ≡ snd y
-        hh = arrowIsSet _ _ (snd x) (snd y)
+        hh = arrowsAreSets _ _ (snd x) (snd y)
       in h i , hh i
 
     module _ {A B : Object} {f : Arrow A B} where
@@ -183,7 +183,7 @@ module _ {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where
       eqUni = foo Y.univalent
       IC.isAssociative      (done i) = propIsAssociative x X.isAssociative Y.isAssociative i
       IC.isIdentity      (done i) = isIdentity i
-      IC.arrowIsSet (done i) = propArrowIsSet x X.arrowIsSet Y.arrowIsSet i
+      IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i
       IC.univalent  (done i) = eqUni i
 
   propIsCategory : isProp (IsCategory C)
@@ -218,7 +218,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     OpIsCategory : IsCategory OpRaw
     IsCategory.isAssociative OpIsCategory = sym isAssociative
     IsCategory.isIdentity OpIsCategory = swap isIdentity
-    IsCategory.arrowIsSet OpIsCategory = arrowIsSet
+    IsCategory.arrowsAreSets OpIsCategory = arrowsAreSets
     IsCategory.univalent OpIsCategory = {!!}
 
   Opposite : Category ℓa ℓb
@@ -244,7 +244,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
     rawIsCat : (i : I) → IsCategory (rawOp i)
     isAssociative (rawIsCat i) = IsCat.isAssociative
     isIdentity (rawIsCat i) = IsCat.isIdentity
-    arrowIsSet (rawIsCat i) = IsCat.arrowIsSet
+    arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets
     univalent (rawIsCat i) = IsCat.univalent
 
   Opposite-is-involution : Opposite (Opposite ℂ) ≡ ℂ

src/Cat/Category/Functor.agda

@@ -55,8 +55,8 @@ module _
 
   propIsFunctor : isProp (IsFunctor _ _ F)
   propIsFunctor isF0 isF1 i = record
-    { isIdentity = 𝔻.arrowIsSet _ _ isF0.isIdentity isF1.isIdentity i
+    { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i
-    ; distrib = 𝔻.arrowIsSet _ _ isF0.distrib isF1.distrib i
+    ; distrib = 𝔻.arrowsAreSets _ _ isF0.distrib isF1.distrib i
     }
     where
       module isF0 = IsFunctor isF0