# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374542844 -32400
# Node ID b518af3a9b071a12fbbfc3ccfd9c534edf4f9805
# Parent  d2b5be1143bf5d5ab79adb19da5b5092abb2427d
on goging

diff -r d2b5be1143bf -r b518af3a9b07 universal-mapping.agda
--- a/universal-mapping.agda	Tue Jul 23 10:13:09 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 10:27:24 2013 +0900
@@ -254,8 +254,12 @@
        sym ( begin
           ε b o (FMap F' (FMap U f))
        ≈⟨⟩
-          ε b o (FMap F' (FMap U f))
+          ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
+       ≈⟨⟩
+          ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
        ≈⟨ {!!} ⟩
+          f o  ((_* um) ( id1 A (FObj U a)))
+       ≈⟨⟩
           f o  (ε a)
        ∎ )
     myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε