chore: flip Algebra-on.ν-mult

This makes it more consistent with ν-unit.

Author: ncfavier

src/Algebra/Group/Cat/Monadic.lagda.md

@@ -92,24 +92,24 @@ is indeed a group structure, which is an incredibly boring calculation.
     assoc : ∀ x y z → mult x (mult y z) ≡ mult (mult x y) z
     assoc x y z = sym $
       ν (inc (ν (inc x ◆ inc y)) ◆ inc z)                ≡⟨ (λ i → ν (inc (ν (inc x ◆ inc y)) ◆ inc (ν-unit (~ i) z))) ⟩
-      ν (inc (ν (inc x ◆ inc y)) ◆ inc (ν (inc z)))      ≡⟨ happly ν-mult (inc _ ◆ inc _) ⟩
+      ν (inc (ν (inc x ◆ inc y)) ◆ inc (ν (inc z)))      ≡˘⟨ happly ν-mult (inc _ ◆ inc _) ⟩
       ν (T.mult.η G (inc (inc x ◆ inc y) ◆ inc (inc z))) ≡˘⟨ ap ν (f-assoc _ _ _) ⟩
-      ν (T.mult.η G (inc (inc x) ◆ inc (inc y ◆ inc z))) ≡˘⟨ happly ν-mult (inc _ ◆ inc _) ⟩
+      ν (T.mult.η G (inc (inc x) ◆ inc (inc y ◆ inc z))) ≡⟨ happly ν-mult (inc _ ◆ inc _) ⟩
       ν (inc (ν (inc x)) ◆ inc (ν (inc y ◆ inc z)))      ≡⟨ (λ i → ν (inc (ν-unit i x) ◆ inc (ν (inc y ◆ inc z)))) ⟩
       ν (inc x ◆ inc (ν (inc y ◆ inc z)))                ∎
 
     invl : ∀ x → mult (ν (inv (inc x))) x ≡ ν nil
     invl x =
       ν (inc (ν (inv (inc x))) ◆ inc x)                ≡⟨ (λ i → ν (inc (ν (inv (inc x))) ◆ inc (ν-unit (~ i) x))) ⟩
-      ν (inc (ν (inv (inc x))) ◆ inc (ν (inc x)))      ≡⟨ happly ν-mult (inc _ ◆ inc _) ⟩
+      ν (inc (ν (inv (inc x))) ◆ inc (ν (inc x)))      ≡˘⟨ happly ν-mult (inc _ ◆ inc _) ⟩
       ν (T.mult.η G (inc (inv (inc x)) ◆ inc (inc x))) ≡⟨ ap ν (f-invl _) ⟩
       ν (T.mult.η G (inc nil))                         ≡⟨⟩
       ν nil                                            ∎
 
     idl' : ∀ x → mult (ν nil) x ≡ x
     idl' x =
       ν (inc (ν nil) ◆ inc x)            ≡⟨ (λ i → ν (inc (ν nil) ◆ inc (ν-unit (~ i) x))) ⟩
-      ν (inc (ν nil) ◆ inc (ν (inc x)))  ≡⟨ happly ν-mult (inc _ ◆ inc _) ⟩
+      ν (inc (ν nil) ◆ inc (ν (inc x)))  ≡˘⟨ happly ν-mult (inc _ ◆ inc _) ⟩
       ν (T.mult.η G (nil ◆ inc (inc x))) ≡⟨ ap ν (f-idl _) ⟩
       ν (inc x)                          ≡⟨ happly ν-unit x ⟩
       x                                  ∎
@@ -174,14 +174,14 @@ but the other direction is by induction on "words".
     module G = Group-on grp
 
     alg-gh : is-group-hom (Free-Group ⌞ x ⌟ .snd) grp (x .snd .ν)
-    alg-gh .is-group-hom.pres-⋆ x y = sym (happly (alg .ν-mult) (inc _ ◆ inc _))
+    alg-gh .is-group-hom.pres-⋆ x y = happly (alg .ν-mult) (inc _ ◆ inc _)
 
     go : rec .fst ≡ x .snd .ν
     go = funext $ Free-elim-prop _ (λ _ → hlevel 1)
       (λ x → sym (happly (alg .ν-unit) x))
       (λ x p y q → rec .snd .is-group-hom.pres-⋆ x y
                 ∙∙ ap₂ G._⋆_ p q
-                ∙∙ happly (alg .ν-mult) (inc _ ◆ inc _))
+                ∙∙ sym (happly (alg .ν-mult) (inc _ ◆ inc _)))
       (λ x p → is-group-hom.pres-inv (rec .snd) {x = x}
               ∙∙ ap G.inverse p
               ∙∙ sym (is-group-hom.pres-inv alg-gh {x = x}))

src/Algebra/Monoid/Category.lagda.md

@@ -295,19 +295,19 @@ these data assembles into a monoid:
         { has-is-magma = record { has-is-set = A .is-tr }
         ; associative  = λ {x} {y} {z} →
           alg .ν (⌜ x ⌝ ∷ alg .ν (y ∷ z ∷ []) ∷ [])               ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
-          alg .ν (alg .ν (x ∷ []) ∷ alg .ν (y ∷ z ∷ []) ∷ [])     ≡⟨ happly (alg .ν-mult) _ ⟩
-          alg .ν (x ∷ y ∷ z ∷ [])                                 ≡˘⟨ happly (alg .ν-mult) _ ⟩
+          alg .ν (alg .ν (x ∷ []) ∷ alg .ν (y ∷ z ∷ []) ∷ [])     ≡˘⟨ happly (alg .ν-mult) _ ⟩
+          alg .ν (x ∷ y ∷ z ∷ [])                                 ≡⟨ happly (alg .ν-mult) _ ⟩
           alg .ν (alg .ν (x ∷ y ∷ []) ∷ ⌜ alg .ν (z ∷ []) ⌝ ∷ []) ≡⟨ ap! (happly (alg .ν-unit) z) ⟩
           alg .ν (alg .ν (x ∷ y ∷ []) ∷ z ∷ [])                   ∎
         }
       has-is-m .idl {x} =
         alg .ν (alg .ν [] ∷ ⌜ x ⌝ ∷ [])            ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
-        alg .ν (alg .ν [] ∷ alg .ν (x ∷ []) ∷ [])  ≡⟨ happly (alg .ν-mult) _ ⟩
+        alg .ν (alg .ν [] ∷ alg .ν (x ∷ []) ∷ [])  ≡˘⟨ happly (alg .ν-mult) _ ⟩
         alg .ν (x ∷ [])                            ≡⟨ happly (alg .ν-unit) x ⟩
         x                                          ∎
       has-is-m .idr {x} =
         alg .ν (⌜ x ⌝ ∷ alg .ν [] ∷ [])            ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
-        alg .ν (alg .ν (x ∷ []) ∷ alg .ν [] ∷ [])  ≡⟨ happly (alg .ν-mult) _ ⟩
+        alg .ν (alg .ν (x ∷ []) ∷ alg .ν [] ∷ [])  ≡˘⟨ happly (alg .ν-mult) _ ⟩
         alg .ν (x ∷ [])                            ≡⟨ happly (alg .ν-unit) x ⟩
         x                                          ∎
 ```
@@ -321,7 +321,7 @@ can show by induction on the list:
     recover []       = refl
     recover (x ∷ xs) =
       alg .ν (x ∷ fold _ xs ∷ [])               ≡⟨ ap₂ (λ e f → alg .ν (e ∷ f ∷ [])) (sym (happly (alg .ν-unit) x)) (recover xs) ⟩
-      alg .ν (alg .ν (x ∷ []) ∷ alg .ν xs ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
+      alg .ν (alg .ν (x ∷ []) ∷ alg .ν xs ∷ []) ≡˘⟨ happly (alg .ν-mult) _ ⟩
       alg .ν (x ∷ xs ++ [])                     ≡⟨ ap (alg .ν) (++-idr _) ⟩
       alg .ν (x ∷ xs)                           ∎
 ```

src/Cat/Diagram/Monad.lagda.md

@@ -107,7 +107,7 @@ doesn't matter whether you first join then evaluate, or evaluate twice.
 
 ```agda
       ν-unit : ν C.∘ η ob ≡ C.id
-      ν-mult : ν C.∘ M₁ ν ≡ ν C.∘ μ ob
+      ν-mult : ν C.∘ μ ob ≡ ν C.∘ M₁ ν
 ```
 
 <!--
@@ -341,7 +341,7 @@ become those of the $M$-action.
   Free-EM : Functor C (Eilenberg-Moore M)
   Free-EM .F₀ A .fst = M₀ A
   Free-EM .F₀ A .snd .ν = μ A
-  Free-EM .F₀ A .snd .ν-mult = μ-assoc
+  Free-EM .F₀ A .snd .ν-mult = sym μ-assoc
   Free-EM .F₀ A .snd .ν-unit = μ-unitl
 ```
 
@@ -384,7 +384,7 @@ $\cC^M$.
   Free-EM⊣Forget-EM .unit =
     NT M.η M.unit.is-natural
   Free-EM⊣Forget-EM .counit =
-    NT (λ x → ∫hom (x .snd .ν) (sym (x .snd .ν-mult)))
+    NT (λ x → ∫hom (x .snd .ν) (x .snd .ν-mult))
       (λ x y f → ext (sym (f .snd)))
   Free-EM⊣Forget-EM .zig = ext μ-unitr
   Free-EM⊣Forget-EM .zag {x} = x .snd .ν-unit
@@ -457,7 +457,7 @@ Eilenberg-Moore category can be restricted to the Kleisli category.
   Free-Kleisli⊣Forget-Kleisli ._⊣_.unit ._=>_.η = η
   Free-Kleisli⊣Forget-Kleisli ._⊣_.unit .is-natural = unit.is-natural
   Free-Kleisli⊣Forget-Kleisli ._⊣_.counit ._=>_.η ((X , α) , free) =
-    ∫hom (α .ν) (sym (α .ν-mult))
+    ∫hom (α .ν) (α .ν-mult)
   Free-Kleisli⊣Forget-Kleisli ._⊣_.counit .is-natural _ _ f =
     ext (sym (f .snd))
   Free-Kleisli⊣Forget-Kleisli ._⊣_.zig = ext μ-unitr

src/Cat/Diagram/Monad/Action.lagda.md

@@ -89,12 +89,12 @@ module _
     c .fst alg → λ where
       .α → !constⁿ (alg .ν)
       .α-unit → ext λ _ → alg .ν-unit
-      .α-mult → ext λ _ → sym (alg .ν-mult)
+      .α-mult → ext λ _ → alg .ν-mult
     c .snd → is-iso→is-equiv λ where
       .is-iso.from act → λ where
         .ν → act .α .η tt
         .ν-unit → act .α-unit ηₚ tt
-        .ν-mult → sym (act .α-mult ηₚ tt)
+        .ν-mult → act .α-mult ηₚ tt
       .is-iso.rinv act → ext λ _ → refl
       .is-iso.linv alg → ext refl
 ```
@@ -124,7 +124,7 @@ module _ {o ℓ} {C : Precategory o ℓ} {M : Functor C C} (Mᵐ : Monad-on M) w
   Forget-EM-action .α .η (_ , alg) = alg .ν
   Forget-EM-action .α .is-natural _ _ f = sym (f .snd)
   Forget-EM-action .α-unit = ext λ (_ , alg) → alg .ν-unit
-  Forget-EM-action .α-mult = ext λ (_ , alg) → sym (alg .ν-mult)
+  Forget-EM-action .α-mult = ext λ (_ , alg) → alg .ν-mult
 ```
 
 And, second, that this left $M$-action is universal in the sense that
@@ -144,7 +144,7 @@ functors $\cB \to \cC$.
     EM-universal {A = A} act .F₀ b .fst = A .F₀ b
     EM-universal {A = A} act .F₀ b .snd .ν = act .α .η b
     EM-universal {A = A} act .F₀ b .snd .ν-unit = act .α-unit ηₚ b
-    EM-universal {A = A} act .F₀ b .snd .ν-mult = sym (act .α-mult ηₚ b)
+    EM-universal {A = A} act .F₀ b .snd .ν-mult = act .α-mult ηₚ b
     EM-universal {A = A} act .F₁ f .fst = A .F₁ f
     EM-universal {A = A} act .F₁ f .snd = sym (act .α .is-natural _ _ f)
     EM-universal {A = A} act .F-id = ext (A .F-id)
@@ -156,7 +156,7 @@ functors $\cB \to \cC$.
     EM→Action A^M .α .η b = A^M .F₀ b .snd .ν
     EM→Action A^M .α .is-natural _ _ f = sym (A^M .F₁ f .snd)
     EM→Action A^M .α-unit = ext λ b → A^M .F₀ b .snd .ν-unit
-    EM→Action A^M .α-mult = ext λ b → sym (A^M .F₀ b .snd .ν-mult)
+    EM→Action A^M .α-mult = ext λ b → A^M .F₀ b .snd .ν-mult
 ```
 
 Note that the universal action itself is induced by the identity

src/Cat/Diagram/Monad/Extension.lagda.md

@@ -323,7 +323,7 @@ that we shall omit.
       (α.ν ∘ M₁ f) ∘ bind g                    ≡⟨ pullr (bind-naturall _ _) ⟩
       α.ν ∘ bind ⌜ M₁ f ∘ g ⌝                  ≡⟨ ap! (insertl (bind-unit-∘ id)) ⟩
       α.ν ∘ bind (join ∘ unit ∘ M₁ f ∘ g)      ≡⟨ pushr (sym (bind-∘ _ _)) ⟩
-      (α.ν ∘ join) ∘ bind (unit ∘ M₁ f ∘ g)    ≡⟨ pushl (sym $ α.ν-mult) ⟩
+      (α.ν ∘ join) ∘ bind (unit ∘ M₁ f ∘ g)    ≡⟨ pushl α.ν-mult ⟩
       α.ν ∘ M₁ α.ν ∘ bind (unit ∘ M₁ f ∘ g)    ≡⟨ ap (α.ν ∘_) (bind-naturall _ _) ⟩
       α.ν ∘ bind ⌜ M₁ α.ν ∘ unit ∘ M₁ f ∘ g ⌝  ≡⟨ ap! (centralizel (sym $ unit-natural _)) ⟩
       α.ν ∘ bind (unit ∘ (α.ν ∘ M₁ f) ∘ g)     ∎
@@ -350,10 +350,10 @@ The proofs of the monad algebra laws are mercifully short.
 ```agda
     alg .ν-unit = α.ν-unit id
     alg .ν-mult =
-      α.ν id ∘ M₁ (α.ν id) ≡⟨ α.ν-natural _ _ ⟩
-      α.ν (id ∘ α.ν id)    ≡⟨ ap α.ν (idl _) ⟩
-      α.ν (α.ν id)         ≡˘⟨ α.ν-join id ⟩
-      α.ν id ∘ join ∎
+      α.ν id ∘ join        ≡⟨ α.ν-join id ⟩
+      α.ν (α.ν id)         ≡˘⟨ ap α.ν (idl _) ⟩
+      α.ν (id ∘ α.ν id)    ≡˘⟨ α.ν-natural _ _ ⟩
+      α.ν id ∘ M₁ (α.ν id) ∎
 ```
 
 As expected, these two functions constitute an equivalence between monad

src/Cat/Functor/Adjoint/Monadic.lagda.md

@@ -75,7 +75,7 @@ Comparison-EM .F₀ x = R.₀ x , alg where
   alg : Algebra-on R∘L (R.₀ x)
   alg .Algebra-on.ν = R.₁ (adj.counit.ε _)
   alg .Algebra-on.ν-unit = adj.zag
-  alg .Algebra-on.ν-mult = R.weave (adj.counit.is-natural _ _ _)
+  alg .Algebra-on.ν-mult = R.weave (sym $ adj.counit.is-natural _ _ _)
 ```
 
 <details>

src/Cat/Functor/Adjoint/Reflective.lagda.md

@@ -194,7 +194,7 @@ is.
   comp-seso (ob , alg) = F.₀ ob , isom where
     Fo→o : Algebra-hom (R∘L adj) (Comp.₀ (F.₀ ob)) (ob , alg)
     Fo→o .fst = alg .ν
-    Fo→o .snd = sym (alg .ν-mult)
+    Fo→o .snd = alg .ν-mult
 
     o→Fo : Algebra-hom (R∘L adj) (ob , alg) (Comp.₀ (F.₀ ob))
     o→Fo .fst = unit.η _

src/Cat/Functor/Algebra.lagda.md

@@ -458,7 +458,7 @@ the algebraically free monad via extension along $\mathrm{fold}$.
     lift-alg {a = a} α .ν = fold α
     lift-alg {a = a} α .ν-unit = zag
     lift-alg {a = a} α .ν-mult =
-      ap fst $ counit.is-natural (Free.₀ a) (a , α) (counit.ε (a , α))
+      ap fst $ sym $ counit.is-natural (Free.₀ a) (a , α) (counit.ε (a , α))
 ```
 
 Likewise, we can extract an $F$-algebra out of a monad algebra by
@@ -500,7 +500,7 @@ clear, but proving it involves quite a bit of algebra.
     alg* {a = a} α .snd =
       α .ν ∘ roll a                                            ≡⟨ intror (F.annihilate zag) ⟩
       (α .ν ∘ roll a) ∘ (F.₁ (mult a) ∘ F.₁ (unit.η _))        ≡⟨ pull-inner (sym $ fold-roll (roll a)) ⟩
-      α .ν ∘ (mult a ∘ roll (F* a)) ∘ F.₁ (unit.η _)           ≡⟨ dispersel (sym $ α .ν-mult) ⟩
+      α .ν ∘ (mult a ∘ roll (F* a)) ∘ F.₁ (unit.η _)           ≡⟨ dispersel (α .ν-mult) ⟩
       α .ν ∘ Free.₁ (α .ν) .fst ∘ roll (F* a) ∘ F.₁ (unit.η _) ≡⟨ extend-inner (map*-roll (α .ν)) ⟩
       α .ν ∘ roll a ∘ F.₁ (map* (α .ν)) ∘ F.₁ (unit.η _)       ≡⟨ centralizer (F.weave (sym (unit.is-natural _ _ _))) ⟩
       α .ν ∘ (roll a ∘ F.₁ (unit.η _)) ∘ F.₁ (α .ν)            ≡⟨ assoc _ _ _ ⟩

src/Cat/Functor/Monadic/Beck.lagda.md

@@ -141,9 +141,9 @@ proof, and any adjunction presenting $T$ will do.
   open is-coequaliser
   algebra-is-coequaliser
     : is-coequaliser C^T {A = TTA} {B = TA} {E = Aalg}
-      mult fold (∫hom A.ν (sym A.ν-mult))
+      mult fold (∫hom A.ν A.ν-mult)
   algebra-is-coequaliser .coequal = ext $
-    A.ν C.∘ T.mult .η _ ≡˘⟨ A.ν-mult ⟩
+    A.ν C.∘ T.mult .η _ ≡⟨ A.ν-mult ⟩
     A.ν C.∘ T.M₁ A.ν    ∎
 ```
 

src/Cat/Functor/Monadic/Crude.lagda.md

@@ -183,7 +183,7 @@ we're seeking.
     η⁻¹η : adj.unit.η _ .fst C.∘ η⁻¹ ≡ C.id
     ηη⁻¹ : η⁻¹ C.∘ adj.unit.η _ .fst ≡ C.id
 
-    η⁻¹ = preserved .universal {e' = o .snd .ν} (o .snd .ν-mult)
+    η⁻¹ = preserved .universal {e' = o .snd .ν} (sym (o .snd .ν-mult))
 
     η⁻¹η = is-coequaliser.unique₂ preserved
       {e' = U.₁ (has-coeq o .coeq)}

src/Cat/Instances/Algebras/Kan.lagda.md

@@ -130,7 +130,7 @@ property and some tedious computations.
           eq = ext λ j →
             eps .η j C.∘ Ext-action .α .η (p.₀ j) C.∘ M.M₁ (Ext-action .α .η (p.₀ j)) ≡⟨ C.extendl (σ-comm ηₚ j) ⟩
             G.₀ j .snd .ν C.∘ M.M₁ (eps .η j) C.∘ M.M₁ (Ext-action .α .η (p.₀ j))     ≡⟨ C.refl⟩∘⟨ MR.weave (σ-comm ηₚ j) ⟩
-            G.₀ j .snd .ν C.∘ M.M₁ (G.₀ j .snd .ν) C.∘ M.M₁ (M.M₁ (eps .η j))         ≡⟨ C.extendl (G.₀ j .snd .ν-mult) ⟩
+            G.₀ j .snd .ν C.∘ M.M₁ (G.₀ j .snd .ν) C.∘ M.M₁ (M.M₁ (eps .η j))         ≡˘⟨ C.extendl (G.₀ j .snd .ν-mult) ⟩
             G.₀ j .snd .ν C.∘ M.μ (G.₀ j .fst) C.∘ M.M₁ (M.M₁ (eps .η j))             ≡⟨ C.refl⟩∘⟨ M.mult .is-natural _ _ _ ⟩
             G.₀ j .snd .ν C.∘ M.M₁ (eps .η j) C.∘ M.μ (Ext.₀ (p.₀ j))                 ≡˘⟨ C.extendl (σ-comm ηₚ j) ⟩
             eps .η j C.∘ Ext-action .α .η (p.₀ j) C.∘ M.μ (Ext.₀ (p.₀ j))             ∎

src/Cat/Instances/Algebras/Limits.lagda.md

@@ -202,12 +202,12 @@ more complicated.
     apex-algebra .ν-mult = lim-over.unique₂ _
       (λ f → C.pulll $ C.pulll (F.₁ f .snd)
            ∙ C.pullr (sym (M.M-∘ _ _) ∙ ap M.M₁ (lim-over.commutes f)))
+      (λ j → C.pulll (lim-over.factors _ _))
       (λ j → C.pulll (lim-over.factors _ _)
           ∙∙ C.pullr (sym (M.M-∘ _ _) ∙ ap M.M₁ (lim-over.factors _ _) ∙ M.M-∘ _ _)
-          ∙∙ C.extendl (FAlg.ν-mult j)
+          ∙∙ C.extendl (sym (FAlg.ν-mult j))
           ∙∙ ap (FAlg.ν j C.∘_) (M.mult.is-natural _ _ _)
           ∙∙ C.assoc _ _ _)
-      (λ j → C.pulll (lim-over.factors _ _))
 ```
 
 </details>