--- a/nat.agda	Fri Jul 26 19:52:19 2013 +0900
+++ b/nat.agda	Fri Jul 26 20:54:41 2013 +0900
@@ -270,7 +270,7 @@
         ; isFunctor = record
         {      ≈-cong   = ≈-cong
              ; identity = identity
-             ; distr    = distr
+             ; distr    = distr1
         }
      } where
         ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
@@ -289,13 +289,33 @@
           ≈⟨ cdr (fcong T f≈g) ⟩
              TMap μ (b)  o FMap T (KMap g)
           ∎
-        distr :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
-        distr {_} {_} {c} {f} {g} = let open ≈-Reasoning (A) in
+        distr1 :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
+        distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
           begin
              ufmap (g * f)
---          ≈⟨⟩
---             TMap μ (FObj T c)  o FMap T ( (TMap μ (c) o FMap T (KMap g))  o (KMap f))
-          ≈⟨ {!!} ⟩
+          ≈⟨⟩
+             ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g)  o (KMap f)) } )
+          ≈⟨⟩
+             TMap μ (c)  o  FMap T ( TMap μ (c) o (FMap T (KMap g)  o (KMap f)))
+          ≈⟨ cdr ( distr T) ⟩
+             TMap μ (c)  o (( FMap T ( TMap μ (c)) o FMap T  (FMap T (KMap g)  o (KMap f))))
+          ≈⟨ assoc ⟩
+             (TMap μ (c)  o ( FMap T ( TMap μ (c)))) o FMap T  (FMap T (KMap g)  o (KMap f))
+          ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
+             (TMap μ (c)  o ( TMap μ (FObj T c))) o FMap T  (FMap T (KMap g)  o (KMap f))
+          ≈⟨ sym assoc ⟩
+             TMap μ (c)  o (( TMap μ (FObj T c)) o FMap T  (FMap T (KMap g)  o (KMap f)))
+          ≈⟨ cdr (cdr (distr T)) ⟩
+             TMap μ (c)  o (( TMap μ (FObj T c)) o (FMap T  (FMap T (KMap g))  o FMap T (KMap f)))
+          ≈⟨ cdr (assoc) ⟩
+             TMap μ (c)  o ((( TMap μ (FObj T c)) o (FMap T  (FMap T (KMap g))))  o FMap T (KMap f))
+          ≈⟨ sym (cdr (car (nat μ ))) ⟩
+             TMap μ (c)  o ((FMap T (KMap g )  o  TMap μ (b))  o FMap T (KMap f ))
+          ≈⟨ cdr (sym assoc) ⟩
+             TMap μ (c)  o (FMap T (KMap g )  o  ( TMap μ (b)  o FMap T (KMap f )))
+          ≈⟨ assoc ⟩
+             ( TMap μ (c)  o FMap T (KMap g ) )  o  ( TMap μ (b)  o FMap T (KMap f ) )
+          ≈⟨⟩
              ufmap g o ufmap f
           ∎
 
@@ -310,7 +330,7 @@
         ; isFunctor = record
         { ≈-cong   = ≈-cong
              ; identity = identity
-             ; distr    = distr
+             ; distr    = distr1
         }
      } where
         identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
@@ -319,9 +339,9 @@
         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 ] ]
         ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
-        distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
+        distr1 :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
                  ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
-        distr {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
+        distr1 {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
           begin
              KMap (ffmap (A [ g o f ]))
           ≈⟨ {!!} ⟩