# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687762334 -32400
# Node ID 8645a167d76be09f85eb772f5aa7ce4db4be2cf1
# Parent  250e52f15f43c5c13693d1b4c2371a55d01eb417
...

diff -r 250e52f15f43 -r 8645a167d76b src/cardinal.agda
--- a/src/cardinal.agda	Mon Jun 26 10:42:16 2023 +0900
+++ b/src/cardinal.agda	Mon Jun 26 15:52:14 2023 +0900
@@ -116,94 +116,6 @@
 Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx) 
         ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq  } 
 
-Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧  Injection b a → Injection (b - a) b ∧  Injection b (b - a) 
-Bernstein1 {a} {b} a<b ⟪ f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject } , g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject } ⟫ 
-    = ⟪ record { i→ = f0 ; iB = b∋f0 ; inject = f0-inject } , record { i→ = f1 ; iB = b∋f1 ; inject = f1-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) } 
-
-      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
-
-      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) )
-
-      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
-
-      UC : HOD
-      UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix 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
-
-      fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f) ))
-      fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt →  be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where
-            be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a  f) x
-            be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
-            be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt )
-            be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt))
-            be21 = ?
-            g⁻¹ : ( x : Ordinal) → odef (* b) x → Ordinal
-            g⁻¹ x bx = fba _ bx  
-            a∋g⁻¹ : ( x : Ordinal) → (bx : odef (* b) x ) → odef (* a) (g⁻¹ x bx ) 
-            a∋g⁻¹ x bx = a∋fba x bx
-            is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → g⁻¹ (fba x ?) ?  ≡ x
-            is-g⁻¹ {x} bx = begin
-                ? ≡⟨ ? ⟩
-                ? ∎ where
-                   open ≡-Reasoning
-            be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? }  where 
-                be02 : CN x
-                be02 = subst (λ k → odef k x) *iso lt
-                be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal
-                be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi )
-                be14 0 {x} (a-g ax ¬ib) = x
-                be14 (suc i) {x} (next-gf lt _) = fba   ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
-                be05 0 {x} (a-g ax ¬ib) = ax
-                be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt))
-                be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi) 
-                be16 0 {x} (a-g ax ¬ib) = record { y = ?
-                    ; ay = subst (λ k → odef k ? ) (sym *iso) record { i = 0 ; gfix = a-g ? ?} ; x=fy = ? }
-                be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? }
-                be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02)) 
-                be11 = be16 _ (CN.gfix be02)
-
-      gU : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f))) (& UC) 
-      gU = ?
-
-      -- Injection (b - a) b 
-      f0 : (x : Ordinal) → odef (* (b - a)) x → Ordinal
-      f0 x lt with subst (λ k → odef k x) *iso lt
-      ... | ⟪ bx , ¬ax ⟫ = fab (fba x bx) (a∋fba x bx)
-      b∋f0 : (x : Ordinal) (lt : odef (* (b - a)) x) → odef (* b) (f0 x lt)
-      b∋f0 x lt with subst (λ k → odef k x) *iso lt
-      ... | ⟪ bx , ¬ax ⟫ = b∋fab (fba x bx) (a∋fba x bx)
-      f0-inject : (x y : Ordinal) (ltx : odef (* (b - a)) x) (lty : odef (* (b - a)) y) → f0 x ltx ≡ f0 y lty → x ≡ y
-      f0-inject x y ltx lty eq = fba-inject _ _ (b-a⊆b ltx) (b-a⊆b lty) ( fab-inject _ _ (a∋fba x  (b-a⊆b ltx)) (a∋fba y (b-a⊆b lty)) eq )
-
-      -- Injection b (b - a) 
-      f1 : (x : Ordinal) → odef (* b) x → Ordinal
-      f1 x lt = ?
-      b∋f1 : (x : Ordinal) (lt : odef (* b) x) → odef (* (b - a)) (f1 x lt)
-      b∋f1 x lt = ?
-      f1-inject : (x y : Ordinal) (ltx : odef (* b) x) (lty : odef (* b) y) → f1 x ltx ≡ f1 y lty → x ≡ y
-      f1-inject x y ltx lty eq = ?
 
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 Bernstein {a} {b} iab iba = be00 where
@@ -213,11 +125,72 @@
        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 x prev b x<b ixb ibx = prev _ be01 _ be02 (proj1 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) (proj2 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) where
-           be01 : (b - x) o< x
-           be01 = ?
-           be02 : (b - x) o< b
-           be02 = ?
+       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 })= prev _ ? _ ? Uf fU 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
+
+          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) )
+
+          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
+
+          UC : HOD
+          UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix 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
+
+          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 ))  
+
+          fUC = & (Image (& UC) {b} (Injection-⊆ UC⊆a  f) )
+          --   C n → f (C n) 
+          fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f) ))
+          fU = record { i→ = be00 ; iB = λ x lt →  be50 x lt ; inject = ? } where
+                be00 : (x : Ordinal) (lt : odef (* (& UC)) x) → Ordinal
+                be00 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 {x} 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) ))
+                be50 : (x : Ordinal) (lt : odef (* (& UC)) x) 
+                     → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f )))) (be00 x lt)
+                be50 x lt1 =  subst (λ k → odef k (be00 x lt1 )) (sym *iso) be03 where
+                    be02 : CN x
+                    be02 = subst (λ k → odef k x) *iso lt1
+                    be03 : odef (Image (& UC) (Injection-⊆ UC⊆a f )) (be00 x lt1 )
+                    be03 with CN.i be02 | CN.gfix be02
+                    ... | zero | a-g {x} ax ¬ib = record { y = x ; ay = lt1 ; x=fy = fab-refl } 
+                    ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy } = record { y = _ ; ay = lt1 ; x=fy = fab-refl } 
+
+          Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f))) (& UC) 
+          Uf = ?
+
     be00 : OrdBijection a b
     be00 with trio< a b
     ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )