Change to multiplicative terminology for combining finite sequences in semigroups, monoids, and groups

src/analysis/series-metric-abelian-groups.lagda.md

@@ -109,7 +109,7 @@ module _
       ( cons-sum-fin-sequence-type-Ab
         ( ab-Metric-Ab G)
         ( n)
-        ( f ∘ nat-Fin (succ-ℕ n)) refl)
+        ( f ∘ nat-Fin (succ-ℕ n)))
       ( refl) ∙
     is-identity-left-conjugation-Ab (ab-Metric-Ab G) _ _
 ```

src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md

@@ -141,13 +141,14 @@ module _
     seq-geometric-sequence-Commutative-Ring R
       standard-geometric-sequence-Commutative-Ring
 
-  is-geometric-standard-geometric-sequence-Commutative-Ring :
-    is-geometric-sequence-Commutative-Semiring
-      ( commutative-semiring-Commutative-Ring R)
-      ( seq-standard-geometric-sequence-Commutative-Ring)
-  is-geometric-standard-geometric-sequence-Commutative-Ring =
-    is-geometric-seq-geometric-sequence-Commutative-Ring R
-      standard-geometric-sequence-Commutative-Ring
+  abstract
+    is-geometric-standard-geometric-sequence-Commutative-Ring :
+      is-geometric-sequence-Commutative-Semiring
+        ( commutative-semiring-Commutative-Ring R)
+        ( seq-standard-geometric-sequence-Commutative-Ring)
+    is-geometric-standard-geometric-sequence-Commutative-Ring =
+      is-geometric-seq-geometric-sequence-Commutative-Ring R
+        standard-geometric-sequence-Commutative-Ring
 ```
 
 ### The geometric sequences `n ↦ a * rⁿ`
@@ -174,10 +175,11 @@ module _
       ( R)
       ( geometric-mul-pow-nat-Commutative-Ring)
 
-  eq-initial-term-mul-pow-nat-Commutative-Ring :
-    initial-term-mul-pow-nat-Commutative-Ring ＝ a
-  eq-initial-term-mul-pow-nat-Commutative-Ring =
-    right-unit-law-mul-Commutative-Ring R a
+  abstract
+    eq-initial-term-mul-pow-nat-Commutative-Ring :
+      initial-term-mul-pow-nat-Commutative-Ring ＝ a
+    eq-initial-term-mul-pow-nat-Commutative-Ring =
+      right-unit-law-mul-Commutative-Ring R a
 ```
 
 ## Properties
@@ -190,16 +192,17 @@ module _
   (u : geometric-sequence-Commutative-Ring R)
   where
 
-  htpy-seq-standard-geometric-sequence-Commutative-Ring :
-    ( seq-geometric-sequence-Commutative-Ring R
-      ( standard-geometric-sequence-Commutative-Ring R
-        ( initial-term-geometric-sequence-Commutative-Ring R u)
-        ( common-ratio-geometric-sequence-Commutative-Ring R u))) ~
-    ( seq-geometric-sequence-Commutative-Ring R u)
-  htpy-seq-standard-geometric-sequence-Commutative-Ring =
-    htpy-seq-standard-geometric-sequence-Commutative-Semiring
-      ( commutative-semiring-Commutative-Ring R)
-      ( u)
+  abstract
+    htpy-seq-standard-geometric-sequence-Commutative-Ring :
+      ( seq-geometric-sequence-Commutative-Ring R
+        ( standard-geometric-sequence-Commutative-Ring R
+          ( initial-term-geometric-sequence-Commutative-Ring R u)
+          ( common-ratio-geometric-sequence-Commutative-Ring R u))) ~
+      ( seq-geometric-sequence-Commutative-Ring R u)
+    htpy-seq-standard-geometric-sequence-Commutative-Ring =
+      htpy-seq-standard-geometric-sequence-Commutative-Semiring
+        ( commutative-semiring-Commutative-Ring R)
+        ( u)
 ```
 
 ### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
@@ -209,20 +212,21 @@ module _
   {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
   where
 
-  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring :
-    mul-pow-nat-Commutative-Ring R a r ~
-    seq-standard-geometric-sequence-Commutative-Ring R a r
-  htpy-mul-pow-standard-geometric-sequence-Commutative-Ring =
-    htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
-      ( commutative-semiring-Commutative-Ring R)
-      ( a)
-      ( r)
+  abstract
+    htpy-mul-pow-standard-geometric-sequence-Commutative-Ring :
+      mul-pow-nat-Commutative-Ring R a r ~
+      seq-standard-geometric-sequence-Commutative-Ring R a r
+    htpy-mul-pow-standard-geometric-sequence-Commutative-Ring =
+      htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+        ( commutative-semiring-Commutative-Ring R)
+        ( a)
+        ( r)
 
-  initial-term-standard-geometric-sequence-Commutative-Ring :
-    seq-standard-geometric-sequence-Commutative-Ring R a r 0 ＝ a
-  initial-term-standard-geometric-sequence-Commutative-Ring =
-    ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Ring 0)) ∙
-    ( eq-initial-term-mul-pow-nat-Commutative-Ring R a r)
+    initial-term-standard-geometric-sequence-Commutative-Ring :
+      seq-standard-geometric-sequence-Commutative-Ring R a r 0 ＝ a
+    initial-term-standard-geometric-sequence-Commutative-Ring =
+      ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Ring 0)) ∙
+      ( eq-initial-term-mul-pow-nat-Commutative-Ring R a r)
 ```
 
 ```agda
@@ -231,22 +235,23 @@ module _
   (u : geometric-sequence-Commutative-Ring R)
   where
 
-  htpy-mul-pow-geometric-sequence-Commutative-Ring :
-    mul-pow-nat-Commutative-Ring
-      ( R)
-      ( initial-term-geometric-sequence-Commutative-Ring R u)
-      ( common-ratio-geometric-sequence-Commutative-Ring R u) ~
-    seq-geometric-sequence-Commutative-Ring R u
-  htpy-mul-pow-geometric-sequence-Commutative-Ring n =
-    ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
-      ( R)
-      ( initial-term-geometric-sequence-Commutative-Ring R u)
-      ( common-ratio-geometric-sequence-Commutative-Ring R u)
-      ( n)) ∙
-    ( htpy-seq-standard-geometric-sequence-Commutative-Semiring
-      ( commutative-semiring-Commutative-Ring R)
-      ( u)
-      ( n))
+  abstract
+    htpy-mul-pow-geometric-sequence-Commutative-Ring :
+      mul-pow-nat-Commutative-Ring
+        ( R)
+        ( initial-term-geometric-sequence-Commutative-Ring R u)
+        ( common-ratio-geometric-sequence-Commutative-Ring R u) ~
+      seq-geometric-sequence-Commutative-Ring R u
+    htpy-mul-pow-geometric-sequence-Commutative-Ring n =
+      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
+        ( R)
+        ( initial-term-geometric-sequence-Commutative-Ring R u)
+        ( common-ratio-geometric-sequence-Commutative-Ring R u)
+        ( n)) ∙
+      ( htpy-seq-standard-geometric-sequence-Commutative-Semiring
+        ( commutative-semiring-Commutative-Ring R)
+        ( u)
+        ( n))
 ```
 
 ### Constant sequences are geometric with common ratio one
@@ -347,16 +352,15 @@ module _
       equational-reasoning
         sum-standard-geometric-fin-sequence-Commutative-Ring R a r (succ-ℕ n)
         ＝
-          sum-standard-geometric-fin-sequence-Commutative-Ring R a r n +R
-          seq-standard-geometric-sequence-Commutative-Ring R a r n
+          ( sum-standard-geometric-fin-sequence-Commutative-Ring R a r n) +R
+          ( seq-standard-geometric-sequence-Commutative-Ring R a r n)
           by
             cons-sum-fin-sequence-type-Commutative-Ring R
               ( n)
               ( standard-geometric-fin-sequence-Commutative-Ring R
                 ( a)
                 ( r)
                 ( succ-ℕ n))
-              ( refl)
         ＝
           ( (a *R 1/⟨1-r⟩) *R (one-R -R power-Commutative-Ring R n r)) +R
           ( a *R power-Commutative-Ring R n r)
@@ -380,12 +384,12 @@ module _
                 ( refl)
                 ( inv (left-unit-law-mul-Commutative-Ring R _)))
         ＝
-          a *R
+          ( a) *R
           ( (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
             (one-R *R power-Commutative-Ring R n r))
           by inv (left-distributive-mul-add-Commutative-Ring R a _ _)
         ＝
-          a *R
+          ( a) *R
           ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
             ( (1/⟨1-r⟩ *R (one-R -R r)) *R power-Commutative-Ring R n r))
             by
@@ -395,7 +399,7 @@ module _
                   ( refl)
                   ( ap-mul-Commutative-Ring R (inv (pr2 H)) refl))
         ＝
-          a *R
+          ( a) *R
           ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
             ( 1/⟨1-r⟩ *R ((one-R -R r) *R power-Commutative-Ring R n r)))
           by
@@ -405,7 +409,7 @@ module _
                 ( refl)
                 ( associative-mul-Commutative-Ring R _ _ _))
         ＝
-          a *R
+          ( a) *R
           ( 1/⟨1-r⟩ *R
             ( ( one-R -R power-Commutative-Ring R n r) +R
               ( (one-R -R r) *R power-Commutative-Ring R n r)))

src/commutative-algebra/geometric-sequences-commutative-semirings.lagda.md

@@ -174,10 +174,11 @@ module _
       ( R)
       ( geometric-mul-pow-nat-Commutative-Semiring)
 
-  eq-initial-term-mul-pow-nat-Commutative-Semiring :
-    initial-term-mul-pow-nat-Commutative-Semiring ＝ a
-  eq-initial-term-mul-pow-nat-Commutative-Semiring =
-    right-unit-law-mul-Commutative-Semiring R a
+  abstract
+    eq-initial-term-mul-pow-nat-Commutative-Semiring :
+      initial-term-mul-pow-nat-Commutative-Semiring ＝ a
+    eq-initial-term-mul-pow-nat-Commutative-Semiring =
+      right-unit-law-mul-Commutative-Semiring R a
 ```
 
 ## Properties
@@ -190,16 +191,17 @@ module _
   (u : geometric-sequence-Commutative-Semiring R)
   where
 
-  htpy-seq-standard-geometric-sequence-Commutative-Semiring :
-    ( seq-geometric-sequence-Commutative-Semiring R
-      ( standard-geometric-sequence-Commutative-Semiring R
-        ( initial-term-geometric-sequence-Commutative-Semiring R u)
-        ( common-ratio-geometric-sequence-Commutative-Semiring R u))) ~
-    ( seq-geometric-sequence-Commutative-Semiring R u)
-  htpy-seq-standard-geometric-sequence-Commutative-Semiring =
-    htpy-seq-standard-geometric-sequence-Semiring
-      ( semiring-Commutative-Semiring R)
-      ( u)
+  abstract
+    htpy-seq-standard-geometric-sequence-Commutative-Semiring :
+      ( seq-geometric-sequence-Commutative-Semiring R
+        ( standard-geometric-sequence-Commutative-Semiring R
+          ( initial-term-geometric-sequence-Commutative-Semiring R u)
+          ( common-ratio-geometric-sequence-Commutative-Semiring R u))) ~
+      ( seq-geometric-sequence-Commutative-Semiring R u)
+    htpy-seq-standard-geometric-sequence-Commutative-Semiring =
+      htpy-seq-standard-geometric-sequence-Semiring
+        ( semiring-Commutative-Semiring R)
+        ( u)
 ```
 
 ### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
@@ -218,11 +220,12 @@ module _
       ( a)
       ( r)
 
-  initial-term-standard-geometric-sequence-Commutative-Semiring :
-    seq-standard-geometric-sequence-Commutative-Semiring R a r 0 ＝ a
-  initial-term-standard-geometric-sequence-Commutative-Semiring =
-    ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring 0)) ∙
-    ( eq-initial-term-mul-pow-nat-Commutative-Semiring R a r)
+  abstract
+    initial-term-standard-geometric-sequence-Commutative-Semiring :
+      seq-standard-geometric-sequence-Commutative-Semiring R a r 0 ＝ a
+    initial-term-standard-geometric-sequence-Commutative-Semiring =
+      ( inv (htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring 0)) ∙
+      ( eq-initial-term-mul-pow-nat-Commutative-Semiring R a r)
 ```
 
 ```agda
@@ -231,22 +234,23 @@ module _
   (u : geometric-sequence-Commutative-Semiring R)
   where
 
-  htpy-mul-pow-geometric-sequence-Commutative-Semiring :
-    mul-pow-nat-Commutative-Semiring
-      ( R)
-      ( initial-term-geometric-sequence-Commutative-Semiring R u)
-      ( common-ratio-geometric-sequence-Commutative-Semiring R u) ~
-    seq-geometric-sequence-Commutative-Semiring R u
-  htpy-mul-pow-geometric-sequence-Commutative-Semiring n =
-    ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
-      ( R)
-      ( initial-term-geometric-sequence-Commutative-Semiring R u)
-      ( common-ratio-geometric-sequence-Commutative-Semiring R u)
-      ( n)) ∙
-    ( htpy-seq-standard-geometric-sequence-Semiring
-      ( semiring-Commutative-Semiring R)
-      ( u)
-      ( n))
+  abstract
+    htpy-mul-pow-geometric-sequence-Commutative-Semiring :
+      mul-pow-nat-Commutative-Semiring
+        ( R)
+        ( initial-term-geometric-sequence-Commutative-Semiring R u)
+        ( common-ratio-geometric-sequence-Commutative-Semiring R u) ~
+      seq-geometric-sequence-Commutative-Semiring R u
+    htpy-mul-pow-geometric-sequence-Commutative-Semiring n =
+      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+        ( R)
+        ( initial-term-geometric-sequence-Commutative-Semiring R u)
+        ( common-ratio-geometric-sequence-Commutative-Semiring R u)
+        ( n)) ∙
+      ( htpy-seq-standard-geometric-sequence-Semiring
+        ( semiring-Commutative-Semiring R)
+        ( u)
+        ( n))
 ```
 
 ### Constant sequences are geometric with common ratio one
@@ -327,7 +331,6 @@ module _
                 ( a)
                 ( r)
                 ( succ-ℕ n))
-              ( refl)
         ＝
           add-Commutative-Semiring R
             ( seq-standard-geometric-sequence-Commutative-Semiring R a r 0)
@@ -438,9 +441,9 @@ module _
               ( ap-mul-Commutative-Semiring R
                 ( refl)
                 ( htpy-sum-fin-sequence-type-Commutative-Semiring R n
-                  ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
+                  ( ( htpy-mul-pow-standard-geometric-sequence-Commutative-Semiring
                       ( R)
                       ( a)
-                      ( r) ∘
-                    nat-Fin n)))
+                      ( r)) ∘
+                    ( nat-Fin n))))
 ```

src/commutative-algebra/sums-of-finite-families-of-elements-commutative-rings.lagda.md

@@ -76,7 +76,7 @@ module _
     (f : unit → type-Commutative-Ring A) →
     sum-finite-Commutative-Ring A unit-Finite-Type f ＝ f star
   sum-unit-finite-Commutative-Ring =
-    sum-unit-finite-Ring (ring-Commutative-Ring A)
+    sum-unit-finite-type-Ring (ring-Commutative-Ring A)
 ```
 
 ### Sums are homotopy invariant
@@ -197,7 +197,7 @@ module _
     (f : type-Finite-Type A → type-Commutative-Ring R) →
     is-zero-Commutative-Ring R (sum-finite-Commutative-Ring R A f)
   eq-zero-sum-finite-is-empty-Commutative-Ring =
-    eq-zero-sum-finite-is-empty-Ring (ring-Commutative-Ring R) A H
+    is-zero-sum-finite-is-empty-Ring (ring-Commutative-Ring R) A H
 ```
 
 ### The sum over a finite type is the sum over any count for that type

src/commutative-algebra/sums-of-finite-families-of-elements-commutative-semirings.lagda.md

@@ -82,7 +82,7 @@ module _
     (f : unit → type-Commutative-Semiring A) →
     sum-finite-Commutative-Semiring A unit-Finite-Type f ＝ f star
   sum-unit-finite-Commutative-Semiring =
-    sum-unit-finite-Semiring (semiring-Commutative-Semiring A)
+    sum-unit-finite-type-Semiring (semiring-Commutative-Semiring A)
 ```
 
 ### Sums over contractible types
@@ -230,7 +230,7 @@ module _
     (f : type-Finite-Type A → type-Commutative-Semiring R) →
     is-zero-Commutative-Semiring R (sum-finite-Commutative-Semiring R A f)
   eq-zero-sum-finite-is-empty-Commutative-Semiring =
-    eq-zero-sum-finite-is-empty-Semiring (semiring-Commutative-Semiring R) A H
+    is-zero-sum-finite-is-empty-Semiring (semiring-Commutative-Semiring R) A H
 ```
 
 ### The sum over a finite type is the sum over any count for that type