# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688025523 -32400
# Node ID ba377f7d0c40430a8d65f7f2987d61de693bbf75
# Parent  6db21bb5e704edd13e3db11c65cbae550bc4a5a6
...

diff -r 6db21bb5e704 -r ba377f7d0c40 src/cardinal.agda
--- a/src/cardinal.agda	Thu Jun 29 11:17:20 2023 +0900
+++ b/src/cardinal.agda	Thu Jun 29 16:58:43 2023 +0900
@@ -271,37 +271,31 @@
             ... | 0 | a-g ax ¬ib = sym x=fy
             ... | (suc i) | next-gf t ix = sym x=fy
 
-      -- be11 : Injection  (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC)
-      Img∨ : (x : Ordinal) → (bx : odef (* b) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x 
-          ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x
-      Img∨ x bx = be20 where
-            be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x
-            be20 with ∨L＼X {* a} {UC} (a∋fba x bx)
-            ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where
-                 be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x
-                 be21 with CN.i uc | CN.gfix uc
-                 ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = refl } )
-                 ... | suc i | next-gf {x1} {y1} record { y = y ; ay = ay ; x=fy = x=fy }  t
-                   = record { y = y ; ay = subst (λ k → odef k y) (sym *iso) be25 ; x=fy = trans be24 (fab-eq refl) } where
-                     be24 : x ≡ fab y ay
-                     be24 = inject g _ _ bx (b∋fab y ay) x=fy
-                     be25 : odef UC y
-                     be25 = record { i = i ; gfix = t }
-            be20 | case2 ⟪ agx , ncn ⟫ = case2 be21 where
-                 be22 :  ¬ odef (C 0) (fba x bx)  -- condition for g⁻¹
-                 be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 }
-                 be21 :  odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x
-                 be21 = ?
-
       h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal
       h {x} ax with ODC.p∨¬p O ( CN x )
       ... | case1 cn  = fU x (subst (λ k → odef k x ) (sym *iso) cn)
       ... | case2 ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ )
 
       h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal
-      h⁻¹ {x} bx with ODC.p∨¬p O ( CN x )
-      ... | case1 cn  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
-      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) ? )
+      h⁻¹ {x} bx with ODC.p∨¬p O ( CN (fba x bx ))
+      ... | case1 cn  = be63 where -- Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } )
+           be63 : Ordinal
+           be63 with CN.i cn | CN.gfix cn
+           ... | 0 | a-g ax ¬ib = Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } )
+           ... | suc i | next-gf {px} ix t = Uf (fab px ?) (subst (λ k → odef k (fab px ?) ) (sym *iso) 
+               record { y = _ ; ay = subst (λ k → odef k (fab px ?)) (sym *iso) record { i = ? ; gfix = ? } ; x=fy = ? } )
+      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where
+           be61 : ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x
+           be61 record { y = y ; ay = ay ; x=fy = x=fy } = be62 where
+               cny : CN y
+               cny = subst (λ k → odef k y ) *iso ay 
+               be62 : ⊥
+               be62 with CN.i cny | CN.gfix cny
+               ... | 0 | a-g ax ¬ib = ncn record { i = 1 ; gfix = next-gf  record { y = _ ; ay = ax ; x=fy = fba-eq x=fy } (a-g ax ¬ib) }
+               ... | suc i | t = ncn record { i = suc (suc i) ; gfix = next-gf  record { y = _ ; ay = ? ; x=fy = fba-eq x=fy } t }
+           be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
+           be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) be61 ⟫
+
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )