# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688116240 -32400
# Node ID 180caeb6927b7f5f8e46daec7f4d53c3d01326c6
# Parent  c66ee9d43c0573aafd1f9f8e8b706a74feb7f02a
...

diff -r c66ee9d43c05 -r 180caeb6927b src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 16:37:32 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 18:10:40 2023 +0900
@@ -124,10 +124,10 @@
 Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
 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←  = λ x lt → h lt
-       ; fun→  = λ x lt → h⁻¹ lt
-       ; funB  = be70
-       ; funA  = be71
+         fun←  = λ x lt → ?
+       ; fun→  = λ x lt → ?
+       ; funB  = ?
+       ; funA  = ?
        ; fiso← = ?
        ; fiso→ = ? }
  where
@@ -296,46 +296,48 @@
             ... | a-g ax ¬ib = sym x=fy
             ... | next-gf t ix = sym x=fy
 
-      h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal
-      h {x} ax with ODC.p∨¬p O (gfImage 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 } → (ax : odef (* a) x) → gfImage x ∨ (¬ gfImage x) → Ordinal
+      h {x} ax (case1 cn)  = fU x (subst (λ k → odef k x ) (sym *iso) cn )
+      h {x} ax (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 (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
-      ... | case1 cn  = Uf x (subst (λ k → odef k x) (sym *iso) cn)                    --   x ≡ f y
-      ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where     -- ¬ x ≡ f y
+      h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) →  (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x))
+          → Ordinal
+      h⁻¹ {x} bx ( case1 cn)  = Uf x (subst (λ k → odef k x) (sym *iso) cn)                    --   x ≡ f y
+      h⁻¹ {x} bx ( case2 ncn) = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where     -- ¬ x ≡ f y
            be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
            be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
 
-      be70 : (x : Ordinal) (lt : odef (* a) x) → odef (* b) (h lt)
-      be70 x ax = ? 
-      -- with ODC.p∨¬p O ( gfImage x )
-      --... | case1 cn  = be03 (subst (λ k → odef k x) (sym *iso) cn) where    -- make the same condition for Uf
-      --     be03 : (cn : odef (* (& UC)) x) → odef (* b) (fU x cn )
-      --     be03 cn with gfImage.i (subst (λ k → odef k x) *iso cn) | gfImage.gfix (subst (λ k → odef k x) *iso cn )
-      --     ... | zero | a-g ax ¬ib = b∋fab x ax
-      --     ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = b∋fab x
-      --           (subst (odef (* a)) (sym x=fy) (a∋fba (fab y ay) (b∋fab y ay)))
-      --... | case2 ncn = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) 
+      be70 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef (* b) (h lt or )
+      be70 x ax ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where    -- make the same condition for Uf
+           be03 : (cn : odef (* (& UC)) x) → odef (* b) (fU x cn )
+           be03 cn with subst (λ k → odef k x) *iso cn 
+           ... | a-g ax ¬ib = b∋fab x ax
+           ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = b∋fab x
+                 (subst (odef (* a)) (sym x=fy) (a∋fba (fab y ay) (b∋fab y ay)))
+      be70 x ax ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) 
 
-      be71 :  (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx)
-      be71  x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   
-      ... | case1 cn  = be03 (subst (λ k → odef k x) (sym *iso) cn) where
+      be71 :  (x : Ordinal) (bx : odef (* b) x) 
+             → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)   ))
+             → odef (* a) (h⁻¹ bx or )
+      be71  x bx ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where
            be03 : (cn : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* a) (Uf x cn )
            be03 cn with subst (λ k → odef k x ) *iso cn
            ... | record { y = y ; ay = ay ; x=fy = x=fy } = UC⊆a ay
-      ... | case2 ncn = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) be60) ))   where
+      be71 x bx ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) be60) ))   where
            be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
            be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫
 
-      be72 :  (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx) ≡ x
+      be71-1 :  (x : Ordinal) (bx : odef (* b) x) 
+             → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) 
+             → gfImage (h⁻¹ bx (case1 or) )
+      be71-1 x bx cn = subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) cn))  
+
+      be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) 
+      be70-1 = ?
+
+      be72 :  (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx ?) ? ≡ x
       be72 x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) 
-      be72 x bx | case1 img = ? where
-           be73 : gfImage (Uf x (subst (λ k → odef k x) (sym *iso) img ))
-           be73 = ?
-           be74 : Uf x (subst (λ k → odef k x) (sym *iso) img ) ≡ IsImage.y (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) img))
-           be74 = refl
+      be72 x bx | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ?
       be72 x bx | case2 nimg = ?