Terminal object and pullbacks in CommRings (i.e. trivial ring and fib…

…ered products) (#676)

* dist lattice sheaf WIP

* finish def of DLSheaf

* first statement of lemma 1

* minor

* comment

* comment the statement

* trivial ring is terminal (needs cleaning!)

* wip

* rename \cdot-comm

* useful lemma for unique existence

* construct fibered products of ring (TODO: move!)

* move

* make Algebra typecheck again

* add trivial ring

* fix things

* rename and reorganize

* rename limits file

Cubical/Algebra/CommAlgebra/Base.agda

@@ -138,7 +138,7 @@ module _ {R : CommRing ℓ} where
         → CommAlgebra R ℓ
     commAlgebraFromCommRing _⋆_ ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc· = fst S ,
       commalgebrastr 0r 1S _+_ _·_  -_ _⋆_
-        (makeIsCommAlgebra is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·-comm
+        (makeIsCommAlgebra is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
                                   ·Assoc⋆ ⋆DistR ⋆DistL ⋆Lid ⋆Assoc·)
 
 

Cubical/Algebra/CommAlgebra/Instances/FreeCommAlgebra.agda

@@ -114,7 +114,7 @@ _[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
 module Theory {R : CommRing ℓ} {I : Type ℓ'} where
   open CommRingStr (snd R)
          using (0r; 1r)
-         renaming (_·_ to _·r_; _+_ to _+r_; ·-comm to ·r-comm; ·Rid to ·r-rid)
+         renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·Rid to ·r-rid)
 
   module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
     open CommAlgebraStr (A .snd)

Cubical/Algebra/CommAlgebra/Instances/Initial.agda

@@ -26,7 +26,7 @@ module _ ((R , str) : CommRing ℓ) where
                     (makeIsCommAlgebra (isSetRing (CommRing→Ring (R , str)))
                        +Assoc +Rid +Rinv +Comm
                        ·Assoc ·Lid
-                       ·Ldist+ ·-comm
+                       ·Ldist+ ·Comm
                         (λ x y z → sym (·Assoc x y z)) ·Ldist+ ·Rdist+ ·Lid
                          λ x y z → sym (·Assoc x y z)))
 

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -47,7 +47,7 @@ module CommAlgChar (R : CommRing ℓ) where
   CommAlgebraStr.- ACommAlgStr = -_
   CommAlgebraStr._⋆_ ACommAlgStr r a = (φ r) · a
   CommAlgebraStr.isCommAlgebra ACommAlgStr = makeIsCommAlgebra
-   is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·-comm
+   is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
    (λ _ _ x → cong (λ y →  y · x) (pres· φIsHom _ _) ∙ sym (·Assoc _ _ _))
    (λ _ _ x → cong (λ y → y · x) (pres+ φIsHom _ _) ∙ ·Ldist+ _ _ _)
    (λ _ _ _ → ·Rdist+ _ _ _)

Cubical/Algebra/CommRing/Base.agda

@@ -35,7 +35,7 @@ record IsCommRing {R : Type ℓ}
 
   field
     isRing : IsRing 0r 1r _+_ _·_ -_
-    ·-comm : (x y : R) → x · y ≡ y · x
+    ·Comm : (x y : R) → x · y ≡ y · x
 
   open IsRing isRing public
 

Cubical/Algebra/CommRing/FiberedProduct.agda

@@ -0,0 +1,101 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.FiberedProduct where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
+
+private
+  variable
+    ℓ : Level
+
+module _ (A B C : CommRing ℓ) (α : CommRingHom A C) (β : CommRingHom B C) where
+
+  private
+    module A = CommRingStr (snd A)
+    module B = CommRingStr (snd B)
+    module C = CommRingStr (snd C)
+    module α = IsRingHom (snd α)
+    module β = IsRingHom (snd β)
+
+  open CommRingStr
+  open CommRingHoms
+  open IsRingHom
+
+  fbT : Type ℓ
+  fbT = Σ[ ab ∈ fst A × fst B ] (fst α (fst ab) ≡ fst β (snd ab))
+
+  fbT≡ : {x y : fbT} → fst (fst x) ≡ fst (fst y) → snd (fst x) ≡ snd (fst y) → x ≡ y
+  fbT≡ h1 h2 = Σ≡Prop (λ _ → is-set (snd C) _ _) λ i → (h1 i) , (h2 i)
+
+  0fbT : fbT
+  0fbT = (A.0r , B.0r) , α.pres0 ∙ sym β.pres0
+
+  1fbT : fbT
+  1fbT = (A.1r , B.1r) , α.pres1 ∙ sym β.pres1
+
+  _+fbT_ : fbT → fbT → fbT
+  ((a1 , b1) , hab1) +fbT ((a2 , b2) , hab2) =
+    (a1 A.+ a2 , b1 B.+ b2) , α.pres+ a1 a2 ∙∙ (λ i → hab1 i C.+ hab2 i) ∙∙ sym (β.pres+ b1 b2)
+
+  _·fbT_ : fbT → fbT → fbT
+  ((a1 , b1) , hab1) ·fbT ((a2 , b2) , hab2) =
+    (a1 A.· a2 , b1 B.· b2) , α.pres· a1 a2 ∙∙ (λ i → hab1 i C.· hab2 i) ∙∙ sym (β.pres· b1 b2)
+
+  -fbT_ : fbT → fbT
+  -fbT ((a , b) , hab) = (A.- a , B.- b) , α.pres- a ∙∙ cong C.-_ hab ∙∙ sym (β.pres- b)
+
+  fiberedProduct : CommRing ℓ
+  fst fiberedProduct = fbT
+  0r (snd fiberedProduct) = 0fbT
+  1r (snd fiberedProduct) = 1fbT
+  _+_ (snd fiberedProduct) = _+fbT_
+  _·_ (snd fiberedProduct) = _·fbT_
+  -_ (snd fiberedProduct) = -fbT_
+  isCommRing (snd fiberedProduct) =
+    makeIsCommRing (isSetΣSndProp (isSet× (is-set (snd A)) (is-set (snd B))) λ x → is-set (snd C) _ _)
+                   (λ _ _ _ → fbT≡ (A.+Assoc _ _ _) (B.+Assoc _ _ _))
+                   (λ _ → fbT≡ (A.+Rid _) (B.+Rid _))
+                   (λ _ → fbT≡ (A.+Rinv _) (B.+Rinv _))
+                   (λ _ _ → fbT≡ (A.+Comm _ _) (B.+Comm _ _))
+                   (λ _ _ _ → fbT≡ (A.·Assoc _ _ _) (B.·Assoc _ _ _))
+                   (λ _ → fbT≡ (A.·Rid _) (B.·Rid _))
+                   (λ _ _ _ → fbT≡ (A.·Rdist+ _ _ _) (B.·Rdist+ _ _ _))
+                   (λ _ _ → fbT≡ (A.·Comm _ _) (B.·Comm _ _))
+
+  fiberedProductPr₁ : CommRingHom fiberedProduct A
+  fst fiberedProductPr₁ = fst ∘ fst
+  snd fiberedProductPr₁ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
+
+  fiberedProductPr₂ : CommRingHom fiberedProduct B
+  fst fiberedProductPr₂ = snd ∘ fst
+  snd fiberedProductPr₂ = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
+
+  fiberedProductPr₁₂Commutes : compCommRingHom fiberedProduct A C fiberedProductPr₁ α
+                             ≡ compCommRingHom fiberedProduct B C fiberedProductPr₂ β
+  fiberedProductPr₁₂Commutes = RingHom≡ (funExt (λ x → x .snd))
+
+  fiberedProductUnivProp :
+    (D : CommRing ℓ) (h : CommRingHom D A) (k : CommRingHom D B) →
+    compCommRingHom D A C h α ≡ compCommRingHom D B C k β →
+    ∃![ l ∈ CommRingHom D fiberedProduct ]
+        (h ≡ compCommRingHom D fiberedProduct A l fiberedProductPr₁)
+      × (k ≡ compCommRingHom D fiberedProduct B l fiberedProductPr₂)
+  fiberedProductUnivProp D (h , hh) (k , hk) H =
+    uniqueExists f (RingHom≡ refl , RingHom≡ refl)
+                 (λ _ → isProp× (isSetRingHom _ _ _ _) (isSetRingHom _ _ _ _))
+                 (λ { (g , _) (Hh , Hk) →
+                    RingHom≡ (funExt (λ d → fbT≡ (funExt⁻ (cong fst Hh) d)
+                                                 (funExt⁻ (cong fst Hk) d))) })
+    where
+    f : CommRingHom D fiberedProduct
+    fst f d = (h d , k d) , funExt⁻ (cong fst H) d
+    snd f = makeIsRingHom (fbT≡ (hh .pres1) (hk .pres1))
+                          (λ _ _ → fbT≡ (hh .pres+ _ _) (hk .pres+ _ _))
+                          (λ _ _ → fbT≡ (hh .pres· _ _) (hk .pres· _ _))
+

Cubical/Algebra/CommRing/Ideal.agda

@@ -53,7 +53,7 @@ module _ (Ring@(R , str) : CommRing ℓ) where
        ; ·-closedLeft = ·-closedLeft
        ; ·-closedRight = λ r x∈pI →
                        subst-∈p I
-                             (·-comm r _)
+                             (·Comm r _)
                              (·-closedLeft r x∈pI)
        })
        where useSolver : (x : R) → - 1r · x ≡ - x
@@ -77,7 +77,7 @@ module CommIdeal (R' : CommRing ℓ) where
    ·Closed : ∀ {x : R} (r : R) → x ∈p I → r · x ∈p I
 
   ·RClosed :  ∀ {x : R} (r : R) → x ∈p I → x · r ∈p I
-  ·RClosed r x∈pI = subst-∈p I (·-comm _ _) (·Closed r x∈pI)
+  ·RClosed r x∈pI = subst-∈p I (·Comm _ _) (·Closed r x∈pI)
 
  open isCommIdeal
  isPropIsCommIdeal : (I : ℙ R) → isProp (isCommIdeal I)
@@ -238,7 +238,7 @@ module CommIdeal (R' : CommRing ℓ) where
 
  ·iComm⊆ : ∀ (I J : CommIdeal) → (I ·i J) ⊆ (J ·i I)
  ·iComm⊆ I J x = map λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
-                      → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·-comm (α i) (β i)))
+                      → (n , (β , α) , ∀βi∈J , ∀αi∈I , x≡∑αβ ∙ ∑Ext (λ i → ·Comm (α i) (β i)))
 
  ·iComm : ∀ (I J : CommIdeal) → I ·i J ≡ J ·i I
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)

Cubical/Algebra/CommRing/Instances/Int.agda

@@ -22,5 +22,5 @@ isCommRing (snd ℤ) = isCommRingℤ
     isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                  -Cancel Int.+Comm Int.·Assoc
-                                 Int.·Rid ·DistR+ ·Comm
+                                 Int.·Rid ·DistR+ Int.·Comm
 

Cubical/Algebra/CommRing/Instances/Pointwise.agda

@@ -33,4 +33,4 @@ pointwiseRing X R = (X → fst R) , str
            (λ f g h i x → ·Assoc (f x) (g x) (h x) i)
            (λ f i x → ·Rid (f x) i)
            (λ f g h i x → ·Rdist+ (f x) (g x) (h x) i)
-           λ f g i x → ·-comm (f x) (g x) i
+           λ f g i x → ·Comm (f x) (g x) i

Cubical/Algebra/CommRing/Instances/Unit.agda

@@ -0,0 +1,27 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.Instances.Unit where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Unit
+
+open import Cubical.Algebra.Ring
+open import Cubical.Algebra.CommRing
+
+private
+  variable
+    ℓ : Level
+
+open CommRingStr
+
+UnitCommRing : CommRing ℓ-zero
+fst UnitCommRing = Unit
+0r (snd UnitCommRing) = tt
+1r (snd UnitCommRing) = tt
+_+_ (snd UnitCommRing) = λ _ _ → tt
+_·_ (snd UnitCommRing) = λ _ _ → tt
+- snd UnitCommRing = λ _ → tt
+isCommRing (snd UnitCommRing) =
+  makeIsCommRing isSetUnit (λ _ _ _ → refl) (λ { tt → refl }) (λ _ → refl)
+                 (λ _ _ → refl) (λ _ _ _ → refl) (λ { tt → refl })
+                 (λ _ _ _ → refl) (λ _ _ → refl)

Cubical/Algebra/CommRing/Localisation/Base.agda

@@ -111,7 +111,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
 
   +ₚ-symm : (a b : R × S) → (a +ₚ b) ≡ (b +ₚ a)
   +ₚ-symm (r₁ , s₁ , s₁∈S) (r₂ , s₂ , s₂∈S) =
-          ΣPathP (+Comm _ _ , Σ≡Prop (λ x → S' x .snd) (·-comm _ _))
+          ΣPathP (+Comm _ _ , Σ≡Prop (λ x → S' x .snd) (·Comm _ _))
 
   θ : (a a' b : R × S) → a ≈ a' → (a +ₚ b) ≈ (a' +ₚ b)
   θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
@@ -202,7 +202,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
   where
   +ₗ-comm[] : (a b : R × S) → ([ a ] +ₗ [ b ]) ≡ ([ b ] +ₗ [ a ])
   +ₗ-comm[] (r , s , s∈S) (r' , s' , s'∈S) =
-            cong [_] (ΣPathP ((+Comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·-comm _ _)))
+            cong [_] (ΣPathP ((+Comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·Comm _ _)))
 
 
  -- Now for multiplication
@@ -216,7 +216,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
 
   ·ₚ-symm : (a b : R × S) → (a ·ₚ b) ≡ (b ·ₚ a)
   ·ₚ-symm (r₁ , s₁ , s₁∈S) (r₂ , s₂ , s₂∈S) =
-          ΣPathP (·-comm _ _ , Σ≡Prop (λ x → S' x .snd) (·-comm _ _))
+          ΣPathP (·Comm _ _ , Σ≡Prop (λ x → S' x .snd) (·Comm _ _))
 
   θ : (a a' b : R × S) → a ≈ a' → (a ·ₚ b) ≈ (a' ·ₚ b)
   θ (r₁ , s₁ , s₁∈S) (r'₁ , s'₁ , s'₁∈S) (r₂ , s₂ , s₂∈S) ((s , s∈S) , p) = (s , s∈S) , path
@@ -269,7 +269,7 @@ module Loc (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultCl
    where
    ·ₗ-comm[] : (a b : R × S) → [ a ] ·ₗ [ b ] ≡ [ b ] ·ₗ [ a ]
    ·ₗ-comm[] (r , s , s∈S) (r' , s' , s'∈S) =
-             cong [_] (ΣPathP ((·-comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·-comm _ _)))
+             cong [_] (ΣPathP ((·Comm _ _) , Σ≡Prop (λ x → ∈-isProp S' x) (·Comm _ _)))
 
 
 

Cubical/Algebra/CommRing/Localisation/InvertingElements.agda

@@ -120,7 +120,7 @@ module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
  open CommRingStr (snd (R[1/_]AsCommRing R' f)) renaming ( _·_ to _·ᶠ_ ; 1r to 1ᶠ
                                                          ; _+_ to _+ᶠ_ ; 0r to 0ᶠ
                                                          ; ·Lid to ·ᶠ-lid ; ·Rid to ·ᶠ-rid
-                                                         ; ·Assoc to ·ᶠ-assoc ; ·-comm to ·ᶠ-comm)
+                                                         ; ·Assoc to ·ᶠ-assoc ; ·Comm to ·ᶠ-comm)
  open IsRingHom
 
  private
@@ -306,7 +306,7 @@ module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
 
              f ^ (l ∸ m) · f ^ m · (g ^ (l ∸ n) · g ^ n) · r
 
-           ≡⟨ cong (_· r) (·-commAssocSwap _ _ _ _) ⟩
+           ≡⟨ cong (_· r) (·CommAssocSwap _ _ _ _) ⟩
 
              f ^ (l ∸ m) · g ^ (l ∸ n) · (f ^ m · g ^ n) · r
 
@@ -465,15 +465,15 @@ module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
 
               r · ((g · f) ^ m)
 
-            ≡⟨ cong (λ x → r · (x ^ m)) (·-comm _ _) ⟩
+            ≡⟨ cong (λ x → r · (x ^ m)) (·Comm _ _) ⟩
 
               r · ((f · g) ^ m)
 
             ≡⟨ cong (r ·_) ((sym s≡fg^m) ∙ s≡fg^n) ⟩
 
               r · ((f · g) ^ n)
 
-            ≡⟨ cong (λ x → r · (x ^ n)) (·-comm _ _) ⟩
+            ≡⟨ cong (λ x → r · (x ^ n)) (·Comm _ _) ⟩
 
               r · ((g · f) ^ n)
 
@@ -523,7 +523,7 @@ module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
 
              (f · g) ^ l · r · (g · f) ^ m
 
-           ≡⟨ cong (λ x → (f · g) ^ l · r · x ^ m) (·-comm _ _) ⟩
+           ≡⟨ cong (λ x → (f · g) ^ l · r · x ^ m) (·Comm _ _) ⟩
 
              (f · g) ^ l · r · (f · g) ^ m
 
@@ -539,7 +539,7 @@ module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
 
              (f · g) ^ l · r' · (f · g) ^ n
 
-           ≡⟨ cong (λ x → (f · g) ^ l · r' · x ^ n) (·-comm _ _) ⟩
+           ≡⟨ cong (λ x → (f · g) ^ l · r' · x ^ n) (·Comm _ _) ⟩
 
              (f · g) ^ l · r' · (g · f) ^ n
 

Cubical/Algebra/CommRing/Localisation/UniversalProperty.agda

@@ -95,12 +95,12 @@ module _ (R' : CommRing ℓ) (S' : ℙ (fst R')) (SMultClosedSubset : isMultClos
    B = fst B'
    open CommRingStr (snd B') renaming  ( is-set to Bset ; _·_ to _·B_ ; 1r to 1b
                                        ; _+_ to _+B_
-                                       ; ·Assoc to ·B-assoc ; ·-comm to ·B-comm
+                                       ; ·Assoc to ·B-assoc ; ·Comm to ·B-comm
                                        ; ·Lid to ·B-lid ; ·Rid to ·B-rid
                                        ; ·Ldist+ to ·B-ldist-+)
    open Units B' renaming (Rˣ to Bˣ ; RˣMultClosed to BˣMultClosed ; RˣContainsOne to BˣContainsOne)
    open RingTheory (CommRing→Ring B') renaming (·-assoc2 to ·B-assoc2)
-   open CommRingTheory B' renaming (·-commAssocl to ·B-commAssocl ; ·-commAssocSwap to ·B-commAssocSwap)
+   open CommRingTheory B' renaming (·CommAssocl to ·B-commAssocl ; ·CommAssocSwap to ·B-commAssocSwap)
 
    ψ₀ = fst ψ
    module ψ = IsRingHom (snd ψ)

Cubical/Algebra/CommRing/Properties.agda

@@ -40,7 +40,7 @@ module Units (R' : CommRing ℓ) where
   path = r'             ≡⟨ sym (·Rid _) ⟩
          r' · 1r        ≡⟨ cong (r' ·_) (sym rr''≡1) ⟩
          r' · (r · r'') ≡⟨ ·Assoc _ _ _ ⟩
-         (r' · r) · r'' ≡⟨ cong (_· r'') (·-comm _ _) ⟩
+         (r' · r) · r'' ≡⟨ cong (_· r'') (·Comm _ _) ⟩
          (r · r') · r'' ≡⟨ cong (_· r'') rr'≡1 ⟩
          1r · r''       ≡⟨ ·Lid _ ⟩
          r''            ∎
@@ -60,15 +60,15 @@ module Units (R' : CommRing ℓ) where
  ·-rinv r ⦃ r∈Rˣ ⦄ = r∈Rˣ .snd
 
  ·-linv : (r : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ → r ⁻¹ · r ≡ 1r
- ·-linv r ⦃ r∈Rˣ ⦄ = ·-comm _ _ ∙ r∈Rˣ .snd
+ ·-linv r ⦃ r∈Rˣ ⦄ = ·Comm _ _ ∙ r∈Rˣ .snd
 
 
  RˣMultClosed : (r r' : R) ⦃ r∈Rˣ : r ∈ Rˣ ⦄ ⦃ r'∈Rˣ : r' ∈ Rˣ ⦄
               → (r · r') ∈ Rˣ
  RˣMultClosed r r' = (r ⁻¹ · r' ⁻¹) , path
   where
   path : r · r' · (r ⁻¹ · r' ⁻¹) ≡ 1r
-  path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ cong (_· (r ⁻¹ · r' ⁻¹)) (·-comm _ _) ⟩
+  path = r · r' · (r ⁻¹ · r' ⁻¹) ≡⟨ cong (_· (r ⁻¹ · r' ⁻¹)) (·Comm _ _) ⟩
          r' · r · (r ⁻¹ · r' ⁻¹) ≡⟨ ·Assoc _ _ _ ⟩
          r' · r · r ⁻¹ · r' ⁻¹   ≡⟨ cong (_· r' ⁻¹) (sym (·Assoc _ _ _)) ⟩
          r' · (r · r ⁻¹) · r' ⁻¹ ≡⟨ cong (λ x → r' · x · r' ⁻¹) (·-rinv _) ⟩
@@ -105,7 +105,7 @@ module Units (R' : CommRing ℓ) where
   path = r ⁻¹ · r' ⁻¹ · (r · r' · (r · r') ⁻¹)
        ≡⟨ ·Assoc _ _ _ ⟩
          r ⁻¹ · r' ⁻¹ · (r · r') · (r · r') ⁻¹
-       ≡⟨ cong (λ x → r ⁻¹ · r' ⁻¹ · x · (r · r') ⁻¹) (·-comm _ _) ⟩
+       ≡⟨ cong (λ x → r ⁻¹ · r' ⁻¹ · x · (r · r') ⁻¹) (·Comm _ _) ⟩
          r ⁻¹ · r' ⁻¹ · (r' · r) · (r · r') ⁻¹
        ≡⟨ cong (_· (r · r') ⁻¹) (sym (·Assoc _ _ _)) ⟩
          r ⁻¹ · (r' ⁻¹ · (r' · r)) · (r · r') ⁻¹
@@ -214,7 +214,7 @@ module Exponentiation (R' : CommRing ℓ) where
   path = f · g · ((f · g) ^ n)       ≡⟨ cong (f · g ·_) (^-ldist-· f g n) ⟩
          f · g · ((f ^ n) · (g ^ n)) ≡⟨ ·Assoc _ _ _ ⟩
          f · g · (f ^ n) · (g ^ n)   ≡⟨ cong (_· (g ^ n)) (sym (·Assoc _ _ _)) ⟩
-         f · (g · (f ^ n)) · (g ^ n) ≡⟨ cong (λ r → (f · r) · (g ^ n)) (·-comm _ _) ⟩
+         f · (g · (f ^ n)) · (g ^ n) ≡⟨ cong (λ r → (f · r) · (g ^ n)) (·Comm _ _) ⟩
          f · ((f ^ n) · g) · (g ^ n) ≡⟨ cong (_· (g ^ n)) (·Assoc _ _ _) ⟩
          f · (f ^ n) · g · (g ^ n)   ≡⟨ sym (·Assoc _ _ _) ⟩
          f · (f ^ n) · (g · (g ^ n)) ∎
@@ -231,17 +231,16 @@ module CommRingTheory (R' : CommRing ℓ) where
  open CommRingStr (snd R')
  private R = fst R'
 
- ·-commAssocl : (x y z : R) → x · (y · z) ≡ y · (x · z)
- ·-commAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·-comm x y) ∙∙ sym (·Assoc y x z)
+ ·CommAssocl : (x y z : R) → x · (y · z) ≡ y · (x · z)
+ ·CommAssocl x y z = ·Assoc x y z ∙∙ cong (_· z) (·Comm x y) ∙∙ sym (·Assoc y x z)
 
- ·-commAssocr : (x y z : R) → x · y · z ≡ x · z · y
- ·-commAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·-comm y z) ∙∙ ·Assoc x z y
+ ·CommAssocr : (x y z : R) → x · y · z ≡ x · z · y
+ ·CommAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y
 
+ ·CommAssocr2 : (x y z : R) → x · y · z ≡ z · y · x
+ ·CommAssocr2 x y z = ·CommAssocr _ _ _ ∙∙ cong (_· y) (·Comm _ _) ∙∙ ·CommAssocr _ _ _
 
- ·-commAssocr2 : (x y z : R) → x · y · z ≡ z · y · x
- ·-commAssocr2 x y z = ·-commAssocr _ _ _ ∙∙ cong (_· y) (·-comm _ _) ∙∙ ·-commAssocr _ _ _
-
- ·-commAssocSwap : (x y z w : R) → (x · y) · (z · w) ≡ (x · z) · (y · w)
- ·-commAssocSwap x y z w = ·Assoc (x · y) z w ∙∙ cong (_· w) (·-commAssocr x y z)
-                                               ∙∙ sym (·Assoc (x · z) y w)
+ ·CommAssocSwap : (x y z w : R) → (x · y) · (z · w) ≡ (x · z) · (y · w)
+ ·CommAssocSwap x y z w =
+   ·Assoc (x · y) z w ∙∙ cong (_· w) (·CommAssocr x y z) ∙∙ sym (·Assoc (x · z) y w)