Mercurial > hg > Members > kono > Proof > category

changeset 39:77c3a5292a2f

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:51:08 +0900
parents 999e637d14c7
children c34b1cfe9fdc
files universal-mapping.agda
diffstat 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/universal-mapping.agda	Mon Jul 22 17:17:42 2013 +0900
+++ b/universal-mapping.agda	Mon Jul 22 17:51:08 2013 +0900
@@ -77,8 +77,12 @@
          universalMapping a b {f} = 
            let open ≈-Reasoning (A) in
               begin 
-                  A [ FMap U ( Solution A B U F ε f  ) o TMap η a ]
-              ≈⟨ ? ⟩
+                  FMap U ( Solution A B U F ε f  ) o TMap η a 
+              ≈⟨⟩
+                  FMap U (  B [ TMap ε b o FMap F f ] ) o TMap η a 
+              ≈⟨ car (IsFunctor.distr ( isFunctor U )) ⟩
+                 ( (FMap U (TMap ε b))  o (FMap U ( FMap F f )) ) o TMap η a 
+              ≈⟨ {!!} ⟩
                   f
               ∎