# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688195022 -32400
# Node ID a0e8df81a466580f2604052f0817f0f5bc84537f
# Parent  a444ea176011272deeae40b1dfd9c38600b63c85
...

diff -r a444ea176011 -r a0e8df81a466 src/cardinal.agda
--- a/src/cardinal.agda	Sat Jul 01 15:50:34 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 16:03:42 2023 +0900
@@ -423,7 +423,7 @@
       ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) 
          = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 
              ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) })
-      ... | case2 c2  = a-UC-iso11 x  be76 be77 where
+      ... | case2 c2  = trans ? ( a-UC-iso11 x  be76 be77) where
            be76 : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x
            be76 = subst (λ k → odef k x) (sym *iso) ⟪ bx , (λ lt → subst (λ k → odef k x → ⊥) (sym *iso) x₁ lt ) ⟫
            be77 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76)))