Mercurial > hg > Members > kono > Proof > category

changeset 38:999e637d14c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Jul 2013 17:17:42 +0900
parents 2f5f5b4d62fa
children 77c3a5292a2f
files universal-mapping.agda
diffstat 1 files changed, 9 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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
+              ∎
+
+