Mercurial > hg > Members > kono > Proof > category

changeset 50:b518af3a9b07

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on goging
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jul 2013 10:27:24 +0900
parents d2b5be1143bf
children adc6bd3c9270
files universal-mapping.agda
diffstat 1 files changed, 5 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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　ε