Rename (co)prod to (co)product (#1017)

CODINGSTYLE.md

@@ -498,8 +498,8 @@ the story. Here's how we handle indentation and line breaks in the
 - Lastly, we recommend not naming constructions after infix notation of
   operations included in them. Preferring primary prefix notation over infix
   notation can help keep our code consistent. For example, it's preferred to use
-  `commutative-prod` instead of `commutative-×` for denoting the commutativity
-  of cartesian products.
+  `commutative-product` instead of `commutative-×` for denoting the
+  commutativity of cartesian products.
 
 These guidelines are here to make everyone's coding experience more enjoyable
 and productive. As always, your contributions to the `agda-unimath` library are

src/category-theory/composition-operations-on-binary-families-of-sets.lagda.md

@@ -187,7 +187,7 @@ module _
       ( λ x y z w →
         is-prop-iterated-Π 3
           ( λ h g f →
-            is-prop-prod
+            is-prop-product
               ( is-set-type-Set
                 ( hom-set x w)
                 ( comp-hom (comp-hom h g) f)
@@ -229,7 +229,7 @@ module _
       ( e' , left-unit-law-e' , right-unit-law-e') =
       eq-type-subtype
         ( λ x →
-          prod-Prop
+          product-Prop
             ( implicit-Π-Prop A
               ( λ a →
                 implicit-Π-Prop A

src/category-theory/coproducts-in-precategories.lagda.md

@@ -32,10 +32,10 @@ module _
   {l1 l2 : Level} (C : Precategory l1 l2)
   where
 
-  is-coproduct-Precategory :
+  is-coproduct-obj-Precategory :
     (x y p : obj-Precategory C) →
     hom-Precategory C x p → hom-Precategory C y p → UU (l1 ⊔ l2)
-  is-coproduct-Precategory x y p l r =
+  is-coproduct-obj-Precategory x y p l r =
     (z : obj-Precategory C)
     (f : hom-Precategory C x z) →
     (g : hom-Precategory C y z) →
@@ -45,36 +45,37 @@ module _
         ( comp-hom-Precategory C h l ＝ f) ×
         ( comp-hom-Precategory C h r ＝ g))
 
-  coproduct-Precategory : obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
-  coproduct-Precategory x y =
+  coproduct-obj-Precategory :
+    obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
+  coproduct-obj-Precategory x y =
     Σ ( obj-Precategory C)
       ( λ p →
         Σ ( hom-Precategory C x p)
           ( λ l →
             Σ (hom-Precategory C y p)
-              ( is-coproduct-Precategory x y p l)))
+              ( is-coproduct-obj-Precategory x y p l)))
 
   has-all-binary-coproducts : UU (l1 ⊔ l2)
   has-all-binary-coproducts =
-    (x y : obj-Precategory C) → coproduct-Precategory x y
+    (x y : obj-Precategory C) → coproduct-obj-Precategory x y
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2) (t : has-all-binary-coproducts C)
   where
 
-  object-coproduct-Precategory :
+  object-coproduct-obj-Precategory :
     obj-Precategory C → obj-Precategory C → obj-Precategory C
-  object-coproduct-Precategory x y = pr1 (t x y)
+  object-coproduct-obj-Precategory x y = pr1 (t x y)
 
-  inl-coproduct-Precategory :
+  inl-coproduct-obj-Precategory :
     (x y : obj-Precategory C) →
-    hom-Precategory C x (object-coproduct-Precategory x y)
-  inl-coproduct-Precategory x y = pr1 (pr2 (t x y))
+    hom-Precategory C x (object-coproduct-obj-Precategory x y)
+  inl-coproduct-obj-Precategory x y = pr1 (pr2 (t x y))
 
-  inr-coproduct-Precategory :
+  inr-coproduct-obj-Precategory :
     (x y : obj-Precategory C) →
-    hom-Precategory C y (object-coproduct-Precategory x y)
-  inr-coproduct-Precategory x y =
+    hom-Precategory C y (object-coproduct-obj-Precategory x y)
+  inr-coproduct-obj-Precategory x y =
     pr1 (pr2 (pr2 (t x y)))
 
   module _
@@ -83,33 +84,33 @@ module _
     (g : hom-Precategory C y z)
     where
 
-    morphism-out-of-coproduct-Precategory :
-      hom-Precategory C (object-coproduct-Precategory x y) z
-    morphism-out-of-coproduct-Precategory =
+    morphism-out-of-coproduct-obj-Precategory :
+      hom-Precategory C (object-coproduct-obj-Precategory x y) z
+    morphism-out-of-coproduct-obj-Precategory =
       pr1 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g))
 
-    morphism-out-of-coproduct-Precategory-comm-inl :
+    morphism-out-of-coproduct-obj-Precategory-comm-inl :
       comp-hom-Precategory
         ( C)
-        ( morphism-out-of-coproduct-Precategory)
-        ( inl-coproduct-Precategory x y) ＝ f
-    morphism-out-of-coproduct-Precategory-comm-inl =
+        ( morphism-out-of-coproduct-obj-Precategory)
+        ( inl-coproduct-obj-Precategory x y) ＝ f
+    morphism-out-of-coproduct-obj-Precategory-comm-inl =
       pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))
 
-    morphism-out-of-coproduct-Precategory-comm-inr :
+    morphism-out-of-coproduct-obj-Precategory-comm-inr :
       comp-hom-Precategory
         ( C)
-        ( morphism-out-of-coproduct-Precategory)
-        ( inr-coproduct-Precategory x y) ＝ g
-    morphism-out-of-coproduct-Precategory-comm-inr =
+        ( morphism-out-of-coproduct-obj-Precategory)
+        ( inr-coproduct-obj-Precategory x y) ＝ g
+    morphism-out-of-coproduct-obj-Precategory-comm-inr =
       pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (t x y))) z f g)))
 
-    is-unique-morphism-out-of-coproduct-Precategory :
-      (h : hom-Precategory C (object-coproduct-Precategory x y) z) →
-      comp-hom-Precategory C h (inl-coproduct-Precategory x y) ＝ f →
-      comp-hom-Precategory C h (inr-coproduct-Precategory x y) ＝ g →
-      morphism-out-of-coproduct-Precategory ＝ h
-    is-unique-morphism-out-of-coproduct-Precategory h comm1 comm2 =
+    is-unique-morphism-out-of-coproduct-obj-Precategory :
+      (h : hom-Precategory C (object-coproduct-obj-Precategory x y) z) →
+      comp-hom-Precategory C h (inl-coproduct-obj-Precategory x y) ＝ f →
+      comp-hom-Precategory C h (inr-coproduct-obj-Precategory x y) ＝ g →
+      morphism-out-of-coproduct-obj-Precategory ＝ h
+    is-unique-morphism-out-of-coproduct-obj-Precategory h comm1 comm2 =
       ap pr1 ((pr2 (pr2 (pr2 (pr2 (t x y))) z f g)) (h , (comm1 , comm2)))
 
 module _
@@ -119,14 +120,14 @@ module _
   (r : hom-Precategory C y p)
   where
 
-  is-prop-is-coproduct-Precategory :
-    is-prop (is-coproduct-Precategory C x y p l r)
-  is-prop-is-coproduct-Precategory =
+  is-prop-is-coproduct-obj-Precategory :
+    is-prop (is-coproduct-obj-Precategory C x y p l r)
+  is-prop-is-coproduct-obj-Precategory =
     is-prop-iterated-Π 3 (λ z f g → is-property-is-contr)
 
   is-coproduct-prop-Precategory : Prop (l1 ⊔ l2)
-  pr1 is-coproduct-prop-Precategory = is-coproduct-Precategory C x y p l r
-  pr2 is-coproduct-prop-Precategory = is-prop-is-coproduct-Precategory
+  pr1 is-coproduct-prop-Precategory = is-coproduct-obj-Precategory C x y p l r
+  pr2 is-coproduct-prop-Precategory = is-prop-is-coproduct-obj-Precategory
 ```
 
 ## Properties
@@ -146,12 +147,12 @@ module _
   (g : hom-Precategory C x₂ y₂)
   where
 
-  map-coproduct-Precategory :
+  map-coproduct-obj-Precategory :
     hom-Precategory C
-      (object-coproduct-Precategory C t x₁ x₂)
-      (object-coproduct-Precategory C t y₁ y₂)
-  map-coproduct-Precategory =
-    morphism-out-of-coproduct-Precategory C t _ _ _
-      (comp-hom-Precategory C (inl-coproduct-Precategory C t y₁ y₂) f)
-      (comp-hom-Precategory C (inr-coproduct-Precategory C t y₁ y₂) g)
+      (object-coproduct-obj-Precategory C t x₁ x₂)
+      (object-coproduct-obj-Precategory C t y₁ y₂)
+  map-coproduct-obj-Precategory =
+    morphism-out-of-coproduct-obj-Precategory C t _ _ _
+      (comp-hom-Precategory C (inl-coproduct-obj-Precategory C t y₁ y₂) f)
+      (comp-hom-Precategory C (inr-coproduct-obj-Precategory C t y₁ y₂) g)
 ```

src/category-theory/embedding-maps-precategories.lagda.md

@@ -48,7 +48,7 @@ module _
 
   is-embedding-map-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   is-embedding-map-prop-map-Precategory =
-    prod-Prop
+    product-Prop
       ( is-emb-Prop (obj-map-Precategory C D F))
       ( is-fully-faithful-prop-map-Precategory C D F)
 

src/category-theory/embeddings-precategories.lagda.md

@@ -43,7 +43,7 @@ module _
 
   is-embedding-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   is-embedding-prop-map-Precategory =
-    prod-Prop
+    product-Prop
       ( is-functor-prop-map-Precategory C D F)
       ( is-embedding-map-prop-map-Precategory C D F)
 

src/category-theory/exponential-objects-precategories.lagda.md

@@ -40,30 +40,30 @@ module _
   (p : has-all-binary-products-Precategory C)
   where
 
-  is-exponential-Precategory :
+  is-exponential-obj-Precategory :
     (x y e : obj-Precategory C) →
-    hom-Precategory C (object-product-Precategory C p e x) y →
+    hom-Precategory C (object-product-obj-Precategory C p e x) y →
     UU (l1 ⊔ l2)
-  is-exponential-Precategory x y e ev =
+  is-exponential-obj-Precategory x y e ev =
     (z : obj-Precategory C)
-    (f : hom-Precategory C (object-product-Precategory C p z x) y) →
+    (f : hom-Precategory C (object-product-obj-Precategory C p z x) y) →
     ∃!
       ( hom-Precategory C z e)
       ( λ g →
         comp-hom-Precategory C ev
-          ( map-product-Precategory C p g (id-hom-Precategory C)) ＝
+          ( map-product-obj-Precategory C p g (id-hom-Precategory C)) ＝
           ( f))
 
-  exponential-Precategory :
+  exponential-obj-Precategory :
     obj-Precategory C → obj-Precategory C → UU (l1 ⊔ l2)
-  exponential-Precategory x y =
+  exponential-obj-Precategory x y =
     Σ (obj-Precategory C) (λ e →
-    Σ (hom-Precategory C (object-product-Precategory C p e x) y) λ ev →
-      is-exponential-Precategory x y e ev)
+    Σ (hom-Precategory C (object-product-obj-Precategory C p e x) y) λ ev →
+      is-exponential-obj-Precategory x y e ev)
 
   has-all-exponentials-Precategory : UU (l1 ⊔ l2)
   has-all-exponentials-Precategory =
-    (x y : obj-Precategory C) → exponential-Precategory x y
+    (x y : obj-Precategory C) → exponential-obj-Precategory x y
 
 module _
   {l1 l2 : Level} (C : Precategory l1 l2)
@@ -72,40 +72,41 @@ module _
   (x y : obj-Precategory C)
   where
 
-  object-exponential-Precategory : obj-Precategory C
-  object-exponential-Precategory = pr1 (t x y)
+  object-exponential-obj-Precategory : obj-Precategory C
+  object-exponential-obj-Precategory = pr1 (t x y)
 
-  eval-exponential-Precategory :
+  eval-exponential-obj-Precategory :
     hom-Precategory C
-      ( object-product-Precategory C p object-exponential-Precategory x)
+      ( object-product-obj-Precategory C p object-exponential-obj-Precategory x)
       ( y)
-  eval-exponential-Precategory = pr1 (pr2 (t x y))
+  eval-exponential-obj-Precategory = pr1 (pr2 (t x y))
 
   module _
     (z : obj-Precategory C)
-    (f : hom-Precategory C (object-product-Precategory C p z x) y)
+    (f : hom-Precategory C (object-product-obj-Precategory C p z x) y)
     where
 
-    morphism-into-exponential-Precategory :
-      hom-Precategory C z object-exponential-Precategory
-    morphism-into-exponential-Precategory = pr1 (pr1 (pr2 (pr2 (t x y)) z f))
+    morphism-into-exponential-obj-Precategory :
+      hom-Precategory C z object-exponential-obj-Precategory
+    morphism-into-exponential-obj-Precategory =
+      pr1 (pr1 (pr2 (pr2 (t x y)) z f))
 
-    morphism-into-exponential-Precategory-comm :
+    morphism-into-exponential-obj-Precategory-comm :
       ( comp-hom-Precategory C
-        ( eval-exponential-Precategory)
-        ( map-product-Precategory C p
-          ( morphism-into-exponential-Precategory)
+        ( eval-exponential-obj-Precategory)
+        ( map-product-obj-Precategory C p
+          ( morphism-into-exponential-obj-Precategory)
           ( id-hom-Precategory C))) ＝
       ( f)
-    morphism-into-exponential-Precategory-comm =
+    morphism-into-exponential-obj-Precategory-comm =
       pr2 (pr1 (pr2 (pr2 (t x y)) z f))
 
-    is-unique-morphism-into-exponential-Precategory :
-      ( g : hom-Precategory C z object-exponential-Precategory) →
+    is-unique-morphism-into-exponential-obj-Precategory :
+      ( g : hom-Precategory C z object-exponential-obj-Precategory) →
       ( comp-hom-Precategory C
-        ( eval-exponential-Precategory)
-        ( map-product-Precategory C p g (id-hom-Precategory C)) ＝ f) →
-      morphism-into-exponential-Precategory ＝ g
-    is-unique-morphism-into-exponential-Precategory g q =
+        ( eval-exponential-obj-Precategory)
+        ( map-product-obj-Precategory C p g (id-hom-Precategory C)) ＝ f) →
+      morphism-into-exponential-obj-Precategory ＝ g
+    is-unique-morphism-into-exponential-obj-Precategory g q =
       ap pr1 (pr2 (pr2 (pr2 (t x y)) z f) (g , q))
 ```

src/category-theory/functors-precategories.lagda.md

@@ -91,7 +91,7 @@ module _
 
   is-functor-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
   is-functor-prop-map-Precategory =
-    prod-Prop
+    product-Prop
       preserves-comp-hom-prop-map-Precategory
       preserves-id-hom-prop-map-Precategory
 

src/category-theory/gaunt-categories.lagda.md

@@ -96,7 +96,9 @@ module _
 
   is-gaunt-prop-Precategory : Prop (l1 ⊔ l2)
   is-gaunt-prop-Precategory =
-    prod-Prop (is-category-prop-Precategory C) (is-prop-iso-prop-Precategory C)
+    product-Prop
+      ( is-category-prop-Precategory C)
+      ( is-prop-iso-prop-Precategory C)
 
   is-gaunt-Precategory : UU (l1 ⊔ l2)
   is-gaunt-Precategory = type-Prop is-gaunt-prop-Precategory

src/category-theory/isomorphisms-in-large-precategories.lagda.md

@@ -164,7 +164,7 @@ module _
   all-elements-equal-is-iso-Large-Precategory f (g , p , q) (g' , p' , q') =
     eq-type-subtype
       ( λ g →
-        prod-Prop
+        product-Prop
           ( Id-Prop
             ( hom-set-Large-Precategory C Y Y)
             ( comp-hom-Large-Precategory C f g)

src/category-theory/isomorphisms-in-precategories.lagda.md

@@ -201,7 +201,7 @@ module _
     (g , p , q) (g' , p' , q') =
     eq-type-subtype
       ( λ g →
-        prod-Prop
+        product-Prop
           ( Id-Prop
             ( hom-set-Precategory C y y)
             ( comp-hom-Precategory C f g)

src/category-theory/monads-on-precategories.lagda.md

@@ -96,7 +96,7 @@ monad-Precategory l C =
                         ( mu)
                         ( T)))
                   ( λ _ →
-                    prod
+                    product
                       ( comp-natural-transformation-Precategory
                           ( C)
                           ( C)

src/category-theory/precategories.lagda.md

@@ -55,7 +55,7 @@ module _
 
   is-precategory-prop-composition-operation-binary-family-Set : Prop (l1 ⊔ l2)
   is-precategory-prop-composition-operation-binary-family-Set =
-    prod-Prop
+    product-Prop
       ( is-unital-prop-composition-operation-binary-family-Set hom-set comp-hom)
       ( is-associative-prop-composition-operation-binary-family-Set
         ( hom-set)