From b63d5455beef46654be2dac9c7ebf5aed06fec44 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Fri, 1 Dec 2023 15:34:21 +0100
Subject: [PATCH] Work on maybe

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

diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md
index 85914cd..277b89e 100644
--- a/src/Monad/Instance/K/Instance/Maybe.lagda.md
+++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md
@@ -25,8 +25,8 @@ open import Function.Base using (id)
 -->
 
 ```agda
-module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
-open Ambient ambient using ()
+-- TODO arguments c ℓ here!
+module Monad.Instance.K.Instance.Maybe {o ℓ e} where
 ```
 
 # The Maybe Monad as instance of K
@@ -85,12 +85,18 @@ module _ {c ℓ : Level} where
 
   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)
+  maybeFun-comp {A} {B} {C} f g {just _} {just _} i≈j = cong g (cong f i≈j)
 
+  maybeFun-resp-≈ : ∀ {A B : Setoid c ℓ} {f g : A ⟶ B} → f ≋ g → maybeFun f ≋ maybeFun g
+  maybeFun-resp-≈ {A} {B} {f} {g} f≈g {nothing} {nothing} i≈j = i≈j
+  maybeFun-resp-≈ {A} {B} {f} {g} f≈g {just _} {just _} i≈j = f≈g i≈j
 
   η : ∀ (A : Setoid c ℓ) → A ⟶ maybeSetoid A
   η A = record { _⟨$⟩_ = just ; cong = id }
 
+  η-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (η B ∘ f) ≋ (maybeFun f ∘ η A)
+  η-natural {A} {B} f {i} {j} i≈j = cong f i≈j
+
   μ : ∀ (A : Setoid c ℓ) → maybeSetoid (maybeSetoid A) ⟶ maybeSetoid A
   μ A = record { _⟨$⟩_ = app ; cong = λ {i} {j} → cong' i j }
     where
@@ -100,6 +106,10 @@ module _ {c ℓ : Level} where
       cong' : ∀ (i j : Maybe (Maybe (Setoid.Carrier A))) → maybe-eq (maybeSetoid A) i j → maybe-eq A (app i) (app j)
       cong' nothing nothing i≈j = i≈j
       cong' (just i) (just j) i≈j = i≈j
+  
+  μ-natural : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) → (μ B ∘ maybeFun (maybeFun f)) ≋ (maybeFun f ∘ μ A)
+  μ-natural {A} {B} f {nothing} {nothing} i≈j = i≈j
+  μ-natural {A} {B} f {just i} {just j} i≈j = cong (maybeFun f) {i} {j} i≈j
 
   maybeMonad : Monad (Setoids c ℓ)
   maybeMonad = record
@@ -108,15 +118,15 @@ module _ {c ℓ : Level} where
       ; F₁ = maybeFun
       ; identity = λ {A} {x} {y} → maybeFun-id {A = A} {x} {y}
       ; homomorphism = λ {A} {B} {C} {f} {g} {i} {j} → maybeFun-comp {A} {B} {C} f g {i} {j}
-      ; F-resp-≈ = {!   !}
+      ; F-resp-≈ = maybeFun-resp-≈
       }
     ; η = ntHelper (record 
       { η = η 
-      ; commute = {!   !} 
+      ; commute = η-natural 
       })
     ; μ = ntHelper (record 
       { η = μ 
-      ; commute = {!   !} 
+      ; commute = μ-natural 
       })
     ; assoc = {!   !}
     ; sym-assoc = {!   !}