chore: follow the naming convention (#311)

the1lab · Dec 11, 2023 · 6477dac · 6477dac
1 parent c80489f
commit 6477dac
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/Cat/Diagram/Monad.lagda.md b/src/Cat/Diagram/Monad.lagda.md
@@ -215,10 +215,10 @@ module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where
     extensionality-algebra-hom = record { lemma = quote Extensional-Algebra-Hom }
 
   instance
-    Funlike-algebra-hom : ⦃ i : Funlike C.Hom ⦄ → Funlike (Algebra-hom C M)
-    Funlike-algebra-hom ⦃ i ⦄ .Funlike.au = Underlying-Σ ⦃ ua = Funlike.au i ⦄
-    Funlike-algebra-hom ⦃ i ⦄ .Funlike.bu = Underlying-Σ ⦃ ua = Funlike.bu i ⦄
-    Funlike-algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x
+    Funlike-Algebra-hom : ⦃ i : Funlike C.Hom ⦄ → Funlike (Algebra-hom C M)
+    Funlike-Algebra-hom ⦃ i ⦄ .Funlike.au = Underlying-Σ ⦃ ua = Funlike.au i ⦄
+    Funlike-Algebra-hom ⦃ i ⦄ .Funlike.bu = Underlying-Σ ⦃ ua = Funlike.bu i ⦄
+    Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x
 
 module _ {o ℓ} (C : Precategory o ℓ) where
   private module C = Cat.Reasoning C