--- a/maybe-monad.agda	Wed Jul 19 20:38:02 2017 +0900
+++ b/maybe-monad.agda	Wed Jul 19 22:27:35 2017 +0900
@@ -6,6 +6,7 @@
 open import HomReasoning
 open import cat-utility
 open import Relation.Binary.Core
+open import Category.Cat
 
 import Relation.Binary.PropositionalEquality
 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
@@ -42,6 +43,79 @@
      ≈-cong1 x y f g nothing refl = refl
      ≈-cong1 x y f g (just z) refl = refl
 
--- Maybe-η : 1 → A
+-- Maybe-η : 1 → M
+
+open Functor
+open NTrans
+
+Maybe-η : NTrans A A identityFunctor Maybe 
+Maybe-η = record {
+       TMap = λ a → λ(x : a) →  just x ;
+       isNTrans = record {
+            commute = λ {a b : Obj A} {f : Hom A a b} → comm a b f 
+       }
+  } where
+     comm1 : (a b : Obj A) (f : Hom A a b) → (x : a) →
+       (A [ FMap Maybe f o just ]) x ≡ (A [ just o FMap (identityFunctor {_} {_} {_} {A}) f ]) x
+     comm1 a b f x = refl
+     comm : (a b : Obj A) (f : Hom A a b) → 
+        A [ A [ Functor.FMap Maybe f o (λ x → just x) ] ≈
+        A [ (λ x → just x) o FMap (identityFunctor {_} {_} {_} {A} ) f ] ]
+     comm a b f = extensionality A ( λ x → comm1 a b f x )
+
+
+
+-- Maybe-μ : MM → M
 
--- Maybe-μ : AA → A
+Maybe-μ : NTrans  A A ( Maybe ○ Maybe ) Maybe
+Maybe-μ = record {
+       TMap =  λ a →  tmap a
+       ; isNTrans = record {
+            commute = comm 
+       }
+  } where
+     tmap : (a : Obj A) → Hom A (FObj (Maybe ○ Maybe) a) (FObj Maybe a )
+     tmap a nothing = nothing
+     tmap a (just nothing ) = nothing
+     tmap a (just (just x) ) = just x
+     comm1 : (a b : Obj A) (f : Hom A a b) → ( x : maybe ( maybe a) ) → 
+        ( A [ FMap Maybe f o tmap a ] ) x ≡ ( A [ tmap b o FMap (Maybe ○ Maybe) f ]  ) x
+     comm1 a b f nothing = refl
+     comm1 a b f (just nothing )  = refl
+     comm1 a b f (just (just x))  = refl
+     comm : {a b : Obj A} {f : Hom A a b} →
+        A [ A [ FMap Maybe f o tmap a ] ≈ A [ tmap b o FMap (Maybe ○ Maybe) f ] ]
+     comm {a} {b} {f} = extensionality A ( λ x → comm1 a b f x )
+
+MaybeMonad : Monad A Maybe Maybe-η Maybe-μ 
+MaybeMonad = record {
+       isMonad = record {
+           unity1 = unity1
+           ; unity2 = unity2
+           ; assoc  = assoc
+       }  
+   } where
+      unity1-1  : (a : Obj A ) → (x : maybe a) → (A [ TMap Maybe-μ a o TMap Maybe-η (FObj Maybe a) ]) x ≡ id1 A (FObj Maybe a) x
+      unity1-1  a nothing = refl
+      unity1-1  a (just x) = refl
+      unity2-1  : (a : Obj A ) → (x : maybe a) → (A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-η a) ]) x ≡ id1 A (FObj Maybe a) x
+      unity2-1  a nothing = refl
+      unity2-1  a (just x) = refl
+      assoc-1 : (a : Obj A ) → (x : maybe (maybe (maybe a))) → (A [ TMap Maybe-μ a o TMap Maybe-μ (FObj Maybe a) ]) x ≡
+                        (A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-μ a) ]) x
+      assoc-1 a nothing = refl
+      assoc-1 a (just nothing) = refl
+      assoc-1 a (just (just nothing )) = refl
+      assoc-1 a (just (just (just x) )) = refl
+      unity1  : {a : Obj A} →
+        A [ A [ TMap Maybe-μ a o TMap Maybe-η (FObj Maybe a) ] ≈ id1 A (FObj Maybe a) ]
+      unity1  {a} = extensionality A ( λ x → unity1-1 a x )
+      unity2 :  {a : Obj A} →
+        A [ A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-η a) ] ≈ id1 A (FObj Maybe a) ]
+      unity2  {a} = extensionality A ( λ x → unity2-1 a x )
+      assoc :  {a : Obj A} → A [ A [ TMap Maybe-μ a o TMap Maybe-μ (FObj Maybe a) ] ≈
+        A [ TMap Maybe-μ a o FMap Maybe (TMap Maybe-μ a) ] ]
+      assoc  {a} = extensionality A ( λ x → assoc-1 a x )
+
+
+