--- a/nat.agda	Sat Jul 27 13:03:02 2013 +0900
+++ b/nat.agda	Sat Jul 27 14:34:21 2013 +0900
@@ -1,4 +1,10 @@
-
+-- -- -- -- -- -- -- -- 
+--  Monad to Kelisli Category
+--  defines U_T and F_T as a resolution of Monad
+--  checks Adjointness
+-- 
+--   Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+-- -- -- -- -- -- -- -- 
 
 -- Monad
 -- Category A
@@ -36,11 +42,13 @@
       → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
 Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )
 
+-- Laws of Monad
+--
 -- η :   1_A → T
 -- μ :   TT → T
--- μ(a)η(T(a)) = a
--- μ(a)T(η(a)) = a
--- μ(a)(μ(T(a))) = μ(a)T(μ(a))
+-- μ(a)η(T(a)) = a                 -- unity law 1
+-- μ(a)T(η(a)) = a                 -- unity law 2
+-- μ(a)(μ(T(a))) = μ(a)T(μ(a))     -- association law
 
 
 open Monad
@@ -76,19 +84,13 @@
     →  A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
 Lemma6 = \m → IsMonad.unity2 ( isMonad m )
 
--- T = M x A
+-- Laws of Kleisli Category
+--
 -- nat of η
--- g ○ f = μ(c) T(g) f
--- η(b) ○ f = f
--- f ○ η(a) = f
--- h ○ (g ○ f) = (h ○ g) ○ 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 ] ]
-lemma12 L x y =  
-   let open ≈-Reasoning ( L )  in 
-      begin  L [ x o y ]  ∎
+-- g ○ f = μ(c) T(g) f        -- join definition
+-- η(b) ○ f = f               -- left id  (Lemma7)
+-- f ○ η(a) = f               -- right id  (Lemma8)
+-- h ○ (g ○ f) = (h ○ g) ○ f  -- assocation law (Lemma9)
 
 open Kleisli
 -- η(b) ○ f = f
@@ -188,6 +190,9 @@
      join K ( join K h g) f 
   ∎ where open ≈-Reasoning (A) 
 
+--
+--  o-resp in Kleisli Category ( for Functor definitions )
+--
 Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
                           A [ f ≈ g ] → A [ h ≈ i ] → A [ (join K h f) ≈ (join K i g) ]
 Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
@@ -201,6 +206,9 @@
        join K i g
    ∎
 
+--
+--  Hom in Kleisli Category
+--
 
 record KHom (a : Obj A)  (b : Obj A)
      : Set c₂ where
@@ -231,17 +239,11 @@
          open ≈-Reasoning (A) 
          isEquivalence :  { a b : Obj A } ->
                IsEquivalence {_} {_} {KHom a b} _⋍_
-         isEquivalence {C} {D} =
-           record { refl  = λ {F} → ⋍-refl {F}
-             ; sym   = λ {F} {G} → ⋍-sym {F} {G}
-             ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
-             } where
-                  ⋍-refl : {F : KHom C D} → F ⋍ F
-                  ⋍-refl = refl-hom
-                  ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F
-                  ⋍-sym = sym
-                  ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H
-                  ⋍-trans = trans-hom
+         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
+           record { refl  = refl-hom
+             ; sym   = sym
+             ; trans = trans-hom
+             } 
          KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
          KidL {_} {_} {f} =  Lemma7 (KMap f) 
          KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
@@ -263,6 +265,13 @@
          ; isCategory = isKleisliCategory
          }
 
+--
+-- Resolution
+--    T = U_T U_F
+--      nat-ε
+--      nat-η
+--
+
 ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
 ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
 
@@ -336,6 +345,7 @@
      } where
         identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
         identity {a} = IsCategory.identityR ( Category.isCategory A)
+        --  Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl
         lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b  ≈  TMap η b ]
         lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
         ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ]
@@ -377,6 +387,10 @@
              KMap  ( ffmap g * ffmap f )
           ∎
 
+--
+-- T = (U_T ○ F_T) 
+--
+
 Lemma11-1 :  ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f  ≈ FMap (U_T ○ F_T) f ]
 Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in
      sym ( begin
@@ -397,9 +411,15 @@
            FMap T f 
      ∎ )
 
+-- construct ≃
+
 Lemma11 :  T ≃  (U_T ○ F_T)
 Lemma11 f = Category.Cat.refl (Lemma11-1 f)
 
+--
+-- natural transformations
+--
+
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
        naturality1 :  {a b : Obj A} {f : Hom A a b}
@@ -465,6 +485,9 @@
        isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
        isNTrans1 = record { naturality = naturality1 } 
 
+--
+-- μ = U_T ε U_F
+--
 Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma12 {x} = let open ≈-Reasoning (A) in
           sym ( begin
@@ -521,7 +544,7 @@
                   TMap η (FObj F_T a)
                ≈⟨⟩
                   KMap (id1 KleisliCategory (FObj F_T a))
-              ∎
+               ∎