# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374481062 -32400
# Node ID 999e637d14c72b37de7cc8bb408b1d821ed8311b
# Parent  2f5f5b4d62fa2e210f167f6f903c98cfc3bfec2d
reasoning

diff -r 2f5f5b4d62fa -r 999e637d14c7 universal-mapping.agda
--- a/universal-mapping.agda	Mon Jul 22 17:11:05 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 17:17:42 2013 +0900
@@ -74,4 +74,12 @@
       } where
          universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
                      A [ A [ FMap U ( Solution A B U F ε f  ) o TMap η a' ]  ≈ f ]
-         universalMapping a b  = ?
+         universalMapping a b {f} = 
+           let open ≈-Reasoning (A) in
+              begin 
+                  A [ FMap U ( Solution A B U F ε f  ) o TMap η a ]
+              ≈⟨ ? ⟩
+                  f
+              ∎
+
+