# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375336891 -32400
# Node ID 32ef4cdb18a2b3c7060a347520510b7b9838fce9
# Parent  3249505073624e7a56300615bfd0f9dcd58d43ba
nat-μ

diff -r 324950507362 -r 32ef4cdb18a2 em-category.agda
--- a/em-category.agda	Thu Aug 01 10:30:54 2013 +0900
+++ b/em-category.agda	Thu Aug 01 15:01:31 2013 +0900
@@ -286,6 +286,12 @@
 -- μ = U^T ε U^F
 --
 
+b : Obj A
+b = {!!}
+
+f : {a : Obj A} -> Hom A a b
+f = {!!}
+
 emap-μ :  (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
 emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
 
@@ -293,7 +299,18 @@
 nat-μ = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
         naturality1 : {a b : Obj A} {f : Hom A a b}
              →  A [ A [ (FMap (U^T ○ F^T) f) o  ( emap-μ a) ]  ≈ A [ ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)  ] ]
-        naturality1 = {!!}
+        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+          sym ( begin 
+             ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) 
+          ≈⟨⟩
+             (FMap U^T ( TMap ε^T ( FObj F^T b ))) o  (FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) )
+          ≈⟨⟩
+             (TMap μ b) o (FMap T (FMap T f))
+          ≈⟨ sym (nat μ) ⟩
+              FMap T f  o ( TMap μ a )
+          ≈⟨⟩
+             (FMap (U^T ○ F^T) f) o  ( emap-μ a)
+          ∎  )
         isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
         isNTrans1 = record { naturality = naturality1 }