Mercurial > hg > Members > kono > Proof > category

changeset 940:6847eba130bd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 17 May 2020 09:24:40 +0900
parents d918ab22419f
children d26f21112e1c
files CCCGraph.agda
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Sun May 17 09:17:39 2020 +0900
+++ b/CCCGraph.agda	Sun May 17 09:24:40 2020 +0900
@@ -384,7 +384,7 @@
     eff : (a : Obj Cart) (f : vertex (g21 (fobj a)) ) → edge (g21 (fobj a)) f f
     eff a f with giso→ {fobj a} {_} {_} {id1 (cat a) (vmap (m12 (fobj a)) f )} (id1 (cat a) (vmap (m12 (fobj a)) f )) 
     ... | tt = subst₂ (λ j k → edge (g21 (fobj a)) j k ) mf=f mf=f m  where
-         fuga : {!!} ≡ {!!}
+         fuga : vmap (m12 (fobj a)) ((vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f))) ≡ vmap (m12 (fobj a)) f
          fuga = eq-vertex1 (fobj a) tt
          mf=f : vmap (m21 (fobj a)) (vmap (m12 (fobj a)) f) ≡ f
          mf=f = eq-vertex1 (g21 (fobj a)) (giso← {!!} )