# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687928577 -32400
# Node ID 1c7b0a040d9cc987c0d67fd22b7b862fcea3ca0b
# Parent  59346935f8a45464702bd6e4ba507287fa7d6e23
...

diff -r 59346935f8a4 -r 1c7b0a040d9c src/cardinal.agda
--- a/src/cardinal.agda	Wed Jun 28 08:56:28 2023 +0900
+++ b/src/cardinal.agda	Wed Jun 28 14:02:57 2023 +0900
@@ -122,166 +122,169 @@
 
 
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
-Bernstein {a} {b} iab iba = be00 where
-    be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ 
-    be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥  } 
-          ind a b a<b iab iba where
-       ind :(x : Ordinal) →
-            ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) →
-            (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ 
-       ind a prev b x<b (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) 
-                       ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })= ? where
- 
-          gf : Injection a a
-          gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
-             ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } 
+Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })
+     = record { fun←  = ?
+       ; fun→  = ?
+       ; funB  = ?
+       ; funA  = ?
+       ; fiso← = ?
+       ; fiso→ = ? }
+ where
+      gf : Injection a a
+      gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) 
+         ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } 
 
-          data gfImage : (i : ℕ) (x : Ordinal) → Set n where
-              a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
-              next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→  (ix : IsImage a a gf x) → gfImage (suc i) x
+      data gfImage : (i : ℕ) (x : Ordinal) → Set n where
+          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x
+          next-gf : {x : Ordinal} → {i : ℕ} → (ix : IsImage a a gf x) → (gfiy : gfImage i (IsImage.y ix) ) → gfImage (suc i) x
 
-          a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
-          a∋gfImage 0 {x} (a-g ax ¬ib) = ax
-          a∋gfImage (suc i) {x} (next-gf lt record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
+      a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x
+      a∋gfImage 0 {x} (a-g ax ¬ib) = ax
+      a∋gfImage (suc i) {x} (next-gf record { y = y ; ay = ay ; x=fy = x=fy } lt ) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) )
 
-          C : ℕ → HOD                                               --  Image {& (C i)} {a} (gf i)  does not work
-          C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } 
+      C : ℕ → HOD                                               --  Image {& (C i)} {a} (gf i)  does not work
+      C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } 
 
-          record CN (x : Ordinal) : Set n where
-              field 
-                 i : ℕ
-                 gfix : gfImage i x
+      record CN (x : Ordinal) : Set n where
+          field 
+             i : ℕ
+             gfix : gfImage i x
 
-          UC : HOD
-          UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
+      UC : HOD
+      UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt))  }
 
-          b-UC : HOD
-          b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt)  }
-          
-          --  UC ⊆ * a
-          --     f : UC → Image f UC    is injection
-          --     g : Image f UC → UC    is injection
+      b-UC : HOD
+      b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt)  }
+      
+      --  UC ⊆ * a
+      --     f : UC → Image f UC    is injection
+      --     g : Image f UC → UC    is injection
 
-          UC⊆a : * (& UC) ⊆ * a
-          UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02)  where
-                be02 : CN x
-                be02 = subst (λ k → odef k x) *iso lt
+      UC⊆a : * (& UC) ⊆ * a
+      UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02)  where
+            be02 : CN x
+            be02 = subst (λ k → odef k x) *iso lt
 
-          b-UC⊆b : * (& b-UC) ⊆ * b
-          b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
+      b-UC⊆b : * (& b-UC) ⊆ * b
+      b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )
 
-          open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-
-          fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x}  → fab x ax ≡ fab x ax1
-          fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
+      open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
-          fba-refl : {x : Ordinal } → {bx bx1 : odef (* b) x}  → fba x bx ≡ fba x bx1
-          fba-refl {x} {bx} {bx1} = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
+      fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → fab x ax ≡ fab y ax1
+      fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
 
-          fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → fab x ax ≡ fab y ax1
-          fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
-
-          fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → fba x bx ≡ fba y bx1
-          fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
+      fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y}  → x ≡ y  → fba x bx ≡ fba y bx1
+      fba-eq {x} {x} {bx} {bx1} refl = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 ))  
 
-          be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
-          be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where
-              be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
-              be12 x lt = i→ g x (proj1 be02) where
-                    be02 : odef (* b) x ∧ ( ¬ CN x )
-                    be02 = subst (λ k → odef k x) *iso lt
-              be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt)
-              be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-refl } where
-                    be02 : odef (* b) x ∧ ( ¬ CN x )
-                    be02 = subst (λ k → odef k x) *iso lt
-              be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y
-              be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq
+      be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) ))
+      be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where
+          be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal
+          be12 x lt = i→ g x (proj1 be02) where
+                be02 : odef (* b) x ∧ ( ¬ CN x )
+                be02 = subst (λ k → odef k x) *iso lt
+          be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt)
+          be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-eq refl } where
+                be02 : odef (* b) x ∧ ( ¬ CN x )
+                be02 = subst (λ k → odef k x) *iso lt
+          be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y
+          be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq
 
-          be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
-          be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where
-              be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal
-              be13 x lt with subst (λ k → odef k x) *iso lt 
-              ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay))
-              be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt)
-              be14 x lt with subst (λ k → odef k x) *iso lt 
-              ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
-              be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x)
-                    (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) →
-                    be13 x ltx ≡ be13 y lty → x ≡ y
-              be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty 
-              ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } 
-                   =  trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) 
-         
-          b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx)  ≡ x
-          b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx)
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where
-                    be02 : odef (* b) x ∧ ( ¬ CN x )
-                    be02 = subst (λ k → odef k x) *iso cx
-                    be03 : odef (* b) y ∧ ( ¬ CN y )
-                    be03 = subst (λ k → odef k y) *iso ay
+      be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC)
+      be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } where
+          be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal
+          be13 x lt with subst (λ k → odef k x) *iso lt 
+          ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay))
+          be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt)
+          be14 x lt with subst (λ k → odef k x) *iso lt 
+          ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
+          be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x)
+                (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) →
+                be13 x ltx ≡ be13 y lty → x ≡ y
+          be15 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty 
+          ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } 
+               =  trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) 
+     
+      b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx)  ≡ x
+      b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx)
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where
+                be02 : odef (* b) x ∧ ( ¬ CN x )
+                be02 = subst (λ k → odef k x) *iso cx
+                be03 : odef (* b) y ∧ ( ¬ CN y )
+                be03 = subst (λ k → odef k y) *iso ay
 
-          b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
-          b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
+      b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
+      b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
-          --   C n → f (C n) 
-          fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
-          fU x lt = be03 where
-                be02 : CN x
-                be02 = subst (λ k → odef k x) *iso lt
-                be03 : Ordinal
-                be03 with CN.i be02 | CN.gfix be02
-                ... | zero | a-g {x} ax ¬ib = fab x ax
-                ... | suc i | next-gf gfiy record { y = y ; ay = ay ; x=fy = x=fy } 
-                       = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) ))
+      --   C n → f (C n) 
+      fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
+      fU x lt = be03 where
+            be02 : CN x
+            be02 = subst (λ k → odef k x) *iso lt
+            be03 : Ordinal
+            be03 with CN.i be02 | CN.gfix be02
+            ... | zero | a-g {x} ax ¬ib = fab x ax
+            ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
+                   = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) ))
 
-          --   f (C n) → g (f (C n) ) ≡ C (suc i)
-          Uf : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
-          Uf x lt with subst (λ k → odef k x ) *iso lt
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = y
+      --   f (C n) → g (f (C n) ) ≡ C (suc i)
+      Uf : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
+      Uf x lt with subst (λ k → odef k x ) *iso lt
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = y
 
-          be04 : {x : Ordinal } →  (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx)
-          be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where
-                be02 : CN x
-                be02 = subst (λ k → odef k x) *iso cx
-                be06 :  odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx)
-                be06 with CN.i be02 | CN.gfix be02
-                ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } 
-                ... | suc i | next-gf gfiy record { y = y ; ay = ay ; x=fy = x=fy } 
-                    = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } 
+      be04 : {x : Ordinal } →  (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx)
+      be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where
+            be02 : CN x
+            be02 = subst (λ k → odef k x) *iso cx
+            be06 :  odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx)
+            be06 with CN.i be02 | CN.gfix be02
+            ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
+            ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy 
+                = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
+
+      UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx)  ≡ x
+      UC-iso0 x cx = be03 where
+             be02 : CN x
+             be02 = subst (λ k → odef k x) *iso cx
+             be03 : Uf ( fU x cx ) (be04 cx)  ≡ x
+             be03 with CN.i be02 | CN.gfix be02 | be04 cx
+             ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect  (fU x) cx
+             ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _  ax (UC⊆a ay) x=fy )
+             be03 | suc i | next-gf record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | cb with 
+                      subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1))))  ) *iso cb 
+             ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _  ax (UC⊆a ay) x=fy ) where
+                  ax : odef (* a) x
+                  ax = subst (λ k → odef (* a) k ) (sym x=fx1) ( a∋fba _ (b∋fab x1 ax1) )
 
-          UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx)  ≡ x
-          UC-iso0 x cx = be03 where
-                 be02 : CN x
-                 be02 = subst (λ k → odef k x) *iso cx
-                 be03 : Uf ( fU x cx ) (be04 cx)  ≡ x
-                 be03 with CN.i be02 | CN.gfix be02 | be04 cx
-                 ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect  (fU x) cx
-                 ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _  ax (UC⊆a ay) x=fy )
-                 be03 | suc i | next-gf s record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } | cb with 
-                          subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1))))  ) *iso cb 
-                 ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _  ax (UC⊆a ay) x=fy ) where
-                      ax : odef (* a) x
-                      ax = subst (λ k → odef (* a) k ) (sym x=fx1) ( a∋fba _ (b∋fab x1 ax1) )
+      be08 : {x : Ordinal } →  (cx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)  → odef (* (& UC)) (Uf x cx)
+      be08 {x} cx with subst (λ k → odef k x) *iso cx
+      ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
+
+      UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f)))) x ) → fU ( Uf x cx ) (be08 cx)  ≡ x
+      UC-iso1 x cx = be14 where
+             be14 : fU ( Uf x cx ) (be08 cx)  ≡ x
+             be14 with subst (λ k → odef k x) *iso cx
+             ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay)
+             ... | 0 | a-g ax ¬ib = sym x=fy
+             ... | (suc i) | next-gf t ix = sym x=fy
 
-          be08 : {x : Ordinal } →  (cx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)  → odef (* (& UC)) (Uf x cx)
-          be08 {x} cx with subst (λ k → odef k x) *iso cx
-          ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay
-
-          UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f)))) x ) → fU ( Uf x cx ) (be08 cx)  ≡ x
-          UC-iso1 x cx = be14 where
-                 be14 : fU ( Uf x cx ) (be08 cx)  ≡ x
-                 be14 with subst (λ k → odef k x) *iso cx
-                 ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay)
-                 ... | 0 | a-g ax ¬ib = sym x=fy
-                 ... | (suc i) | next-gf t ix = sym x=fy
-
-
-    be00 : OrdBijection a b
-    be00 with trio< a b
-    ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
-    ... | tri≈ ¬a b ¬c = ordbij-refl b
-    ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )
+      Img∨ : (x : Ordinal) → odef (* b) x → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x 
+      Img∨ x bx = be20 where
+             be20 :  odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) 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 (subst (λ k → odef k x) (sym *iso) be21 ) where
+                 be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) x
+                 be21 = record { y = ? ; ay = ? ; x=fy = ? }
 
 _c<_ : ( A B : HOD ) → Set n
 A c< B = ¬ ( Injection (& A)  (& B) )