--- a/nat.agda	Sat Jul 06 02:15:24 2013 +0900
+++ b/nat.agda	Sat Jul 06 03:30:31 2013 +0900
@@ -7,7 +7,7 @@
 --T(a) = t(a)
 --T(f) = tf(f)
 
-open import Category
+open import Category -- https://github.com/konn/category-agda
 open import Level
 open Functor
 
@@ -65,14 +65,28 @@
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
       assoc  : {a : Obj A} -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
---      unity2 : {a : Obj A} -> A [ Trans μ a o (FMap T (Trans η a )) ]
---      unity1 : {a : Obj A} -> A [ Trans μ a o Trans η ( FObj T a ) ]
+      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η 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
   field
     isMonad : IsMonad A T η μ
 
+open Monad
+Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { a : Obj A } ->
+                 ( M : Monad A T η μ )
+    -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
+Lemma3 = \m -> IsMonad.assoc ( isMonad m )
+
+
+Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
+    -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
+Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
 
 -- nat of η