From 7be2f41196f95a273f02ab8a604976a8701198ab Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Fri, 1 Dec 2023 14:46:36 +0100
Subject: [PATCH] minor

---
 src/Monad/Instance/K/Instance/Maybe.lagda.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md
index 5a5326c..85914cd 100644
--- a/src/Monad/Instance/K/Instance/Maybe.lagda.md
+++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md
@@ -83,6 +83,10 @@ module _ {c ℓ : Level} where
   maybeFun-id {A} {nothing} {nothing} i≈j = i≈j
   maybeFun-id {A} {just _} {just _} i≈j = i≈j
 
+  maybeFun-comp : ∀ {A B C : Setoid c ℓ} (f : A ⟶ B) (g : B ⟶ C) → maybeFun (g ∘ f) ≋ ((maybeFun g) ∘ (maybeFun f))
+  maybeFun-comp {A} {B} {C} f g {nothing} {nothing} i≈j = i≈j
+  maybeFun-comp {A} {B} {C} f g {just i} {just j} i≈j = cong g (cong f i≈j)
+
 
   η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
   η A = record { _⟨$⟩_ = just ; cong = id }
@@ -103,7 +107,7 @@ module _ {c ℓ : Level} where
       { F₀ = maybeSetoid
       ; F₁ = maybeFun
       ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
-      ; homomorphism = {!   !}
+      ; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
       ; F-resp-≈ = {!   !}
       }
     ; η = ntHelper (record