# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1373635043 -32400
# Node ID d9c2386a18a8f19a72984f5ac54368f6016fab11
# Parent  ad62c87659ef7d5c7871259b7958b78b589fd7e5
fix

diff -r ad62c87659ef -r d9c2386a18a8 nat.agda
--- a/nat.agda	Fri Jul 12 20:45:54 2013 +0900
+++ b/nat.agda	Fri Jul 12 22:17:23 2013 +0900
@@ -181,6 +181,9 @@
   infixr 2 _≈⟨_⟩_ 
   infix  1 begin_
 
+------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
+--  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  -> A [ x ≈  y ] -> x ≡ y
+--  ≈-to-≡ refl-hom = refl
 
   data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
@@ -290,7 +293,7 @@
      A [ Trans μ d  o A [ FMap T h  o  A [ Trans μ c o A [ FMap T g  o f ] ] ] ]
    ≈⟨ cdr-eq ( Trans μ d ) ( cdr-eq ( FMap T h ) ( assoc )) ⟩
      A [ Trans μ d  o A [ FMap T h  o  A [ A [ Trans μ c o  FMap T g ]  o f ] ] ]
-   ≈⟨ assoc  ⟩    ---   A [ f x A [ g x h ] ] = A [ A [ f x g ] x h ]
+   ≈⟨ assoc  ⟩    ---   A [ f  o  A [ g  o  h ] ] = A [ A [ f  o  g ]  o  h ]
      A [     A [ Trans μ d o  FMap T h ] o  A [ A [ Trans μ c o  FMap T g ]  o f ] ]
    ≈⟨ assoc  ⟩
      A [ A [ A [ Trans μ d o      FMap T h ] o  A [ Trans μ c  o  FMap T g ] ] o f ]
@@ -315,7 +318,13 @@
      A [ A [ Trans μ d  o  A [ Trans μ ( FObj T d)     o FMap T ( A [ FMap T h  o g ] ) ] ]   o f ]
    ≈⟨ car-eq f assoc ⟩
      A [ A [ A [ Trans μ d  o  Trans μ ( FObj T d)   ]  o FMap T ( A [ FMap T h  o g ] ) ]    o f ]
-   ≈⟨ car-eq f ( car-eq  (FMap T ( A [ FMap T h  o g ] )) ( IsMonad.assoc ( isMonad m ))) ⟩
+   ≈⟨ car-eq f ( car-eq  (FMap T ( A [ FMap T h  o g ] )) ( 
+      begin
+         A [ Trans μ d o Trans μ (FObj T d) ]
+      ≈⟨ IsMonad.assoc ( isMonad m) ⟩
+         A [ Trans μ d o FMap T (Trans μ d) ]
+      ∎
+   )) ⟩
      A [ A [ A [ Trans μ d  o    FMap T ( Trans μ d) ]  o FMap T ( A [ FMap T h  o g ] ) ]    o f ]
    ≈⟨ car-eq f (sym assoc) ⟩
      A [ A [ Trans μ d  o  A   [ FMap T ( Trans μ d )   o FMap T ( A [ FMap T h  o g ] ) ] ]  o f ]