chore: flip Coalgebra-on.ρ-comult

Author: ncfavier

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

@@ -76,7 +76,7 @@ Comparison-CoEM .F₀ x = L.₀ x , alg where
   alg : Coalgebra-on L∘R (L.₀ x)
   alg .Coalgebra-on.ρ = L.₁ (adj.unit.η _)
   alg .Coalgebra-on.ρ-counit = adj.zig
-  alg .Coalgebra-on.ρ-comult = L.weave (sym (adj.unit.is-natural _ _ _))
+  alg .Coalgebra-on.ρ-comult = L.weave (adj.unit.is-natural _ _ _)
 ```
 
 <details>

src/Cat/Instances/Coalgebras.lagda.md

@@ -58,7 +58,7 @@ module _ {o ℓ} {C : Precategory o ℓ} {W : Functor C C} (cm : Comonad-on W) w
     field
       ρ        : Hom A (W₀ A)
       ρ-counit : W.ε A ∘ ρ ≡ id
-      ρ-comult : W₁ ρ ∘ ρ ≡ δ A ∘ ρ
+      ρ-comult : δ A ∘ ρ ≡ W₁ ρ ∘ ρ
 ```
 
 This definition is rather abstract, but has a nice intuition in terms of
@@ -233,7 +233,7 @@ gives us **cofree coalgebras**.
   Cofree-coalgebra A .fst = W₀ A
   Cofree-coalgebra A .snd .ρ = δ _
   Cofree-coalgebra A .snd .ρ-counit = δ-unitr
-  Cofree-coalgebra A .snd .ρ-comult = δ-assoc
+  Cofree-coalgebra A .snd .ρ-comult = sym δ-assoc
 
   Cofree : Functor C (Coalgebras W)
   Cofree .F₀ = Cofree-coalgebra
@@ -251,7 +251,7 @@ the forgetful functor, we get a right adjoint!
 ```agda
   Forget⊣Cofree : πᶠ (Coalgebras-over W) ⊣ Cofree
   Forget⊣Cofree .unit .η (x , α) .fst = α .ρ
-  Forget⊣Cofree .unit .η (x , α) .snd = α .ρ-comult
+  Forget⊣Cofree .unit .η (x , α) .snd = sym (α .ρ-comult)
   Forget⊣Cofree .unit .is-natural x y f = ext (sym (f .snd))
 
   Forget⊣Cofree .counit .η x              = W.ε x

src/Cat/Instances/Coalgebras/Cartesian.lagda.md

@@ -351,12 +351,12 @@ formalised proof is a bit annoying, it's hidden in this
         {p = W.extendl (f .snd)
           ∙∙ ap₂ _∘_ refl wit
           ∙∙ W.extendl (sym (g .snd))}
-        (pulll (W.weave p'.p₁∘universal) ∙ pullr p'.p₁∘universal)
-        (pulll (W.weave p'.p₂∘universal) ∙ pullr p'.p₂∘universal)
-        (pulll (sym (comult.is-natural _ _ _)) ∙∙ pullr p'.p₁∘universal ∙∙ extendl (sym α.ρ-comult))
+        (pulll (sym (comult.is-natural _ _ _)) ∙∙ pullr p'.p₁∘universal ∙∙ extendl α.ρ-comult)
         (  pulll (sym (comult.is-natural _ _ _))
         ∙∙ pullr p'.p₂∘universal
-        ∙∙ extendl (sym β.ρ-comult))
+        ∙∙ extendl β.ρ-comult)
+        (pulll (W.weave p'.p₁∘universal) ∙ pullr p'.p₁∘universal)
+        (pulll (W.weave p'.p₂∘universal) ∙ pullr p'.p₂∘universal)
 ```
 
 </details>

src/Cat/Instances/Coalgebras/Colimits.lagda.md

@@ -109,12 +109,12 @@ module _ {jo jℓ} {J : Precategory jo jℓ} (F : Functor J (Coalgebras W)) wher
     coapex-coalgebra .ρ-comult = colim-over.unique₂ _
       (λ f → C.pullr $ C.pullr (sym (F.₁ f .snd))
            ∙ C.pulll (sym (W.W-∘ _ _) ∙ ap W.W₁ (colim-over.commutes f)))
-      (λ j → C.pullr (colim-over.factors _ _))
       (λ j → C.pullr (colim-over.factors _ _)
            ∙ sym (C.pulll (sym (W.W-∘ _ _) ∙ ap W.W₁ (colim-over.factors _ _) ∙ W.W-∘ _ _)
-               ∙∙ C.extendr (FAlg.ρ-comult j)
+               ∙∙ C.extendr (sym (FAlg.ρ-comult j))
                ∙∙ ap (C._∘ FAlg.ρ j) (sym (W.comult.is-natural _ _ _))
                 ∙ sym (C.assoc _ _ _)))
+      (λ j → C.pullr (colim-over.factors _ _))
 ```
 
 <!--

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

@@ -229,10 +229,10 @@ To show that $\eps \nu = \id$, it will suffice to show that $\psi_j \eps
       (λ f → W.extendl (F.₁ f .snd) ∙ ap₂ _∘_ refl
         ( pulll (F.₁ f .snd)
         ∙ pullr (sym (L.eps .is-natural _ _ f) ∙ elimr L.Ext.F-id)))
-      (λ j → W.extendl ν-β ∙ ap₂ _∘_ refl ν-β)
       (λ j → pulll (sym (comult.is-natural _ _ _))
           ∙∙ pullr ν-β
-          ∙∙ extendl (sym (F.₀ j .snd .ρ-comult)))
+          ∙∙ extendl (F.₀ j .snd .ρ-comult))
+      (λ j → W.extendl ν-β ∙ ap₂ _∘_ refl ν-β)
 
   open Ran
   open is-ran