From 6477dacdb0a1a7f2863939a9333937b16041a777 Mon Sep 17 00:00:00 2001 From: favonia Date: Mon, 11 Dec 2023 11:51:13 -0600 Subject: [PATCH] chore: follow the naming convention (#311) --- src/Cat/Diagram/Monad.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Cat/Diagram/Monad.lagda.md b/src/Cat/Diagram/Monad.lagda.md index b6bc305c6..928361497 100644 --- 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