# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1373629554 -32400
# Node ID ad62c87659ef7d5c7871259b7958b78b589fd7e5
# Parent  8117bafdec7a4ebf50b354b1095759a76dbc57b3
join association finish

diff -r 8117bafdec7a -r ad62c87659ef nat.agda
--- a/nat.agda	Fri Jul 12 20:32:19 2013 +0900
+++ b/nat.agda	Fri Jul 12 20:45:54 2013 +0900
@@ -300,15 +300,14 @@
      A [ A [ Trans μ d o  A [ A [ FMap T h o      Trans μ c ]  o  FMap T g ]   ] o f ]
    ≈⟨ car-eq f assoc ⟩
      A [ A [ A [ Trans μ d o  A [ FMap T h   o  Trans μ c ] ]  o  FMap T g ] o f ]
---   ≈⟨ car-eq f (cdr-eq  ( Trans μ d ) ( sym ( nat A μ))) ⟩
    ≈⟨ car-eq f (car-eq ( FMap T g) ( cdr-eq  ( Trans μ d ) ( begin 
-           {!!}
-       ≈⟨ {!!} ⟩
-           {!!}
+           A [ FMap T h o Trans μ c ]
+       ≈⟨ nat A μ ⟩
+           A [ Trans μ (FObj T d) o FMap T (FMap T h) ]
         ∎ 
    )))  ⟩
       A [ A [ A [ Trans μ d  o  A [ Trans μ ( FObj T d)    o  FMap T (  FMap T h ) ] ]  o FMap T g ]  o f ]
-   ≈⟨ {!!} ⟩
+   ≈⟨ car-eq f (sym assoc) ⟩
      A [ A [ Trans μ d  o  A [ A [ Trans μ ( FObj T d)     o FMap T (  FMap T h ) ]   o FMap T g ] ]   o f ]
    ≈⟨ car-eq f ( cdr-eq ( Trans μ d ) (sym assoc) ) ⟩
      A [ A [ Trans μ d  o  A [ Trans μ ( FObj T d)     o A [ FMap T (  FMap T h ) o FMap T g ] ] ]   o f ]