--- a/nat.agda	Tue Jul 23 17:34:46 2013 +0900
+++ b/nat.agda	Wed Jul 24 20:47:28 2013 +0900
@@ -9,7 +9,9 @@
 
 open import Category -- https://github.com/konn/category-agda
 open import Level
-open import Category.HomReasoning
+--open import Category.HomReasoning
+open import HomReasoning
+open import cat-utility
 
 --T(g f) = T(g) T(f)
 
@@ -33,24 +35,6 @@
 -- μ(a)T(η(a)) = a
 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
 
-record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T)
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-   field
-      assoc  : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-      unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-      unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-
-record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
-       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-  eta : NTrans A A identityFunctor T
-  eta = η
-  mu : NTrans A A (T ○ T) T
-  mu = μ
-  field
-    isMonad : IsMonad A T η μ
 
 open Monad
 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
@@ -92,17 +76,6 @@
 -- f ○ η(a) = f
 -- h ○ (g ○ f) = (h ○ g) ○ f
 
-record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T )
-                 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-     monad : Monad A T η μ 
-     monad = M
-     -- g ○ f = μ(c) T(g) f
-     join : { a b : Obj A } → ( c : Obj A ) →
-                      ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
-     join c g f = A [ TMap μ c  o A [ FMap T g  o f ] ]
 
 lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → 
        ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ]
@@ -110,19 +83,18 @@
    let open ≈-Reasoning ( L )  in 
       begin  L [ x o y ]  ∎
 
-
 open Kleisli
 -- η(b) ○ f = f
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
-                 ( T : Functor A A )
+                 { T : Functor A A }
                  ( η : NTrans A A identityFunctor T )
                  { μ : NTrans A A (T ○ T) T }
                  { a : Obj A } ( b : Obj A ) 
                  ( f : Hom A a ( FObj T b) )
                  ( m : Monad A T η μ )
-                 ( k : Kleisli A T η μ m) 
+                 { k : Kleisli A T η μ m}
                       → A  [ join k b (TMap η b) f  ≈ f ]
-Lemma7 c T η b f m k = 
+Lemma7 c {T} η b f m {k} = 
   let open ≈-Reasoning (c) 
       μ = mu ( monad k )
   in 
@@ -167,17 +139,17 @@
 
 -- h ○ (g ○ f) = (h ○ g) ○ f
 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-                 ( T : Functor A A )
-                 ( η : NTrans A A identityFunctor T )
-                 ( μ : NTrans A A (T ○ T) T )
-                 ( a b c d : Obj A )
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { a b c d : Obj A }
                  ( f : Hom A a ( FObj T b) )
                  ( g : Hom A b ( FObj T c) ) 
                  ( h : Hom A c ( FObj T d) )
                  ( m : Monad A T η μ )
-                 ( k : Kleisli A T η μ m)
+                 { k : Kleisli A T η μ m}
                       → A  [ join k d h (join k c g f)  ≈ join k d ( join k d h g) f ]
-Lemma9 A T η μ a b c d f g h m k = 
+Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 
   begin 
      join k d h (join k c g f)  
    ≈⟨⟩
@@ -231,7 +203,41 @@
      join k d ( join k d h g) f 
   ∎ where open ≈-Reasoning (A) 
 
+-- Kleisli-join : {!!}
+-- Kleisli-join = {!!}
 
+-- Kleisli-id : {!!}
+-- Kleisli-id = {!!}
+
+-- Lemma10 : {!!}
+-- Lemma10 = {!!}
+
+-- open import Relation.Binary.Core
+
+-- isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
+--                  { T : Functor A A }
+--                  { η : NTrans A A identityFunctor T }
+--                  { μ : NTrans A A (T ○ T) T }
+--                  ( m : Monad A T η μ )
+--                  { k : Kleisli A T η μ m} ->
+--          IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
+-- isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
+--                     ; identityL =   {!!}
+--                     ; identityR =   {!!}
+--                     ; o-resp-≈ =    {!!}
+--                     ; associative = {!!}
+--                     }
+--      where
+--          KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
+--                  { η : NTrans A A identityFunctor T }
+--                  { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) -> {!!}
+--          KidL = {!!}
+--          KidR : {!!}
+--          KidR = {!!}
+--          Ko-resp : {!!}
+--          Ko-resp = {!!}
+--          Kassoc : {!!}
+--          Kassoc = {!!}
 
 -- Kleisli :
 -- Kleisli = record { Hom = 
@@ -249,3 +255,20 @@
 --                                        ; associative = associative
 --                                        }
 --                  }
+
+open Adjunction
+
+-- ( \b -> FMap U ( TMap ε ( FObj F b))  )
+Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
+                 { U : Functor B A }
+                 { F : Functor A B }
+                 { η : NTrans A A identityFunctor ( U ○  F ) }
+                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
+      Adjunction A B U F η ε  → Monad A (U ○  F) η {!!}
+Adj2Monad A B {U} {F} {η} {ε} adj = record {
+         isMonad = record {
+                    assoc = {!!};
+                    unity1 = {!!};
+                    unity2 = {!!}
+              }
+      }