# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589675080 -32400
# Node ID 6847eba130bdbe4532eb87de4bd271dbfc0aaba3
# Parent  d918ab22419f05c651cadf12acd8d25e3250ebc3
...

diff -r d918ab22419f -r 6847eba130bd CCCGraph.agda
--- 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← {!!} )