--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Sat Jul 06 00:34:08 2013 +0900
@@ -0,0 +1,94 @@
+
+
+module nat  where 
+
+
+-- Monad
+-- Category A
+
+-- A = Category
+
+-- Functor T : A -> A
+
+
+
+--T(a) = t(a)
+--T(f) = tf(f)
+
+--T(g f) = T(g) T(f)
+
+open import Category
+open import Level
+open Functor
+
+Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) ->  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
+     -> A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
+Lemma1 = \t -> IsFunctor.distr ( isFunctor t )
+
+
+
+
+--        F(f)
+--   F(a) ----> F(b)
+--    |          |
+--    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
+--    |          |
+--    v          v
+--   G(a) ----> G(b)
+--        G(f)
+
+record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
+                 ( F G : Functor D C )
+                 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+  field
+    naturality : {a b : Obj D} {f : Hom D a b} 
+      → C [ C [ (  FMap G f ) o  ( Trans a ) ]  ≈ C [ (Trans b ) o  (FMap F f)  ] ]
+--     how to write uniquness?
+--    uniqness : {d : Obj D} 
+--      →  ∃{e : Trans d} -> ∀{a : Trans d}  → C [ e  ≈ a ]
+
+
+record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
+       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
+  field
+    Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
+    isNTrans : IsNTrans domain codomain F G Trans
+
+open NTrans
+Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b }
+      -> A [ A [  FMap G f  o  Trans μ a  ]  ≈ A [ Trans μ b  o  FMap F f ] ]
+Lemma2 = \n -> IsNTrans.naturality ( isNTrans  n  )
+
+open import Category.Cat
+
+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
+    unity1 : {a b : Obj A} 
+      → A [ A [ ( Trans μ a ) o ( Trans η a) ] ≈ Id A a ]
+
+-- η :   1_A -> T
+-- μ :   TT -> T
+-- μ(a)η(T(a)) = a
+-- μ(a)T(η(a)) = a
+-- μ(a)(μ(T(a))) = μ(a)T(μ(a))
+
+
+
+
+
+-- nat of η
+
+
+-- g ○ f = μ(c) T(g) f
+
+-- h ○ (g ○ f) = (h ○ g) ○ f
+
+-- η(b) ○ f = f
+-- f ○ η(a) = f
+
+