# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688128652 -32400
# Node ID 04bb6152f691f73d35568893b078c9b808894656
# Parent  4d9b60eed3725f0b03fcc474015c9c53690c807d
...

diff -r 4d9b60eed372 -r 04bb6152f691 src/cardinal.agda
--- a/src/cardinal.agda	Fri Jun 30 20:14:26 2023 +0900
+++ b/src/cardinal.agda	Fri Jun 30 21:37:32 2023 +0900
@@ -126,10 +126,10 @@
      = record { 
          fun←  = λ x lt → h lt (cc0 x)
        ; fun→  = λ x lt → h⁻¹ lt (cc1 x)
-       ; funB  = ?
-       ; funA  = ?
-       ; fiso← = λ x lt → be72 x lt (cc1 x) 
-       ; fiso→ = λ x lt → be73 x lt (cc0 x)   
+       ; funB  = be74
+       ; funA  = be75
+       ; fiso← = λ x lt → be72 x lt (cc11 (a∋fba x lt) (cc20 lt))
+       ; fiso→ = λ x lt → be73 x lt (cc10 (b∋fab x lt) (cc21 lt))
        }
  where
       gf : Injection a a
@@ -150,7 +150,16 @@
       a-UC : HOD
       a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ gfImage x) } ; odmax = & (* a) 
           ; <odmax = λ lt → odef< (proj1 lt)  }
-      
+
+      nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a g x
+      nimg {x} ax ncn with ODC.p∨¬p O (IsImage b a g x)
+      ... | case1 img = img
+      ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
+
+      aucimg : {x : Ordinal } → (cx : odef (* (& a-UC)) x ) → IsImage b a g x
+      aucimg {x} cx with subst (λ k → odef k x ) *iso cx
+      ... | ⟪ ax , ncn ⟫ = nimg ax ncn
+
       --  UC ⊆ * a
       --     f : UC → Image f UC    is injection
       --     g : Image f UC → UC    is injection
@@ -176,22 +185,16 @@
           uc00 : gfImage y
           uc00 = subst (λ k → odef k y) *iso uy
 
-      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ (¬ IsImage b a g x) ) → Ordinal
-      g⁻¹ {x} ax nc0  with ODC.p∨¬p O ( IsImage b a g x )
-      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = y
-      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism  )
+      g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a g x ) → Ordinal
+      g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y
 
-      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : ¬ (¬ IsImage b a g x )) → odef (* b) (g⁻¹ ax nc0)
-      b∋g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
-      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ay
-      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism )
+      b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : IsImage b a g x ) → odef (* b) (g⁻¹ ax nc0)
+      b∋g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = ay
 
-      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ (¬ IsImage b a g x )) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
-      g⁻¹-iso {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x )
-      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
-      ... | case2 ¬ism = ⊥-elim ( nc0 ¬ism )
+      g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a g x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x
+      g⁻¹-iso {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy
 
-      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : ¬ (¬ IsImage b a g (fba x bx) ))  → g⁻¹ (a∋fba x bx) nc0  ≡ x
+      g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a g (fba x bx) )  → g⁻¹ (a∋fba x bx) nc0  ≡ x
       g⁻¹-iso1 {x} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) 
 
       be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x
@@ -199,9 +202,9 @@
           be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x
           be15 {x} lt with subst (λ k → odef k x) *iso lt
           ... | ⟪ ax , ncn ⟫ = ax
-          be16 : {x : Ordinal } → odef (* (& a-UC)) x →  ¬ ( ¬ IsImage b a g x )  
-          be16 {x} lt nc0 with subst (λ k → odef k x) *iso lt
-          ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn ? )
+          be16 : {x : Ordinal } → odef (* (& a-UC)) x →  IsImage b a g x 
+          be16 {x} lt with subst (λ k → odef k x) *iso lt
+          ... | ⟪ ax , ncn ⟫ = nimg ax ncn
           be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt))
           be17 x lt = subst ( λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) (sym *iso) ⟪ be19 , 
                  (λ img → be18 be14 (subst (λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) *iso img) )  ⟫  where
@@ -237,8 +240,7 @@
                   be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl)
      
       a-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& a-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx)  ≡ x
-      a-UC-iso0 x cx = trans (fba-eq refl) ( g⁻¹-iso (proj1 ( subst (λ k → odef k x) (*iso) cx )) 
-         (λ cn → ⊥-elim ? ))
+      a-UC-iso0 x cx = trans (fba-eq refl) ( g⁻¹-iso (proj1 ( subst (λ k → odef k x) (*iso) cx )) (aucimg cx))
 
       a-UC-iso1 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx)  ≡ x
       a-UC-iso1 x cx with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) )
@@ -309,6 +311,24 @@
       cc1 : (x : Ordinal) → CC1 x
       cc1 x = ODC.p∨¬p O (odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) 
 
+      cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt )
+      cc20 = ?
+
+      cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt )
+      cc21 = ?
+
+      --
+      --  h    : * a  → * b
+      --  h⁻¹  : * b  → * a
+      --
+      --  it have to accept any alement in a or b
+      --  it is handle by different function fU or gU with exclusive conditon CC0 (p ∨ ¬ p)
+      --     in OrdBijection record, LEM rules are used
+      --  but we cannot use LEM in second function call on iso parts.
+      --  so we have to do some devices.
+      --
+      --  otherwise not strict positive on gfImage error will happen
+
       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 ⟫ ) 
@@ -349,10 +369,23 @@
       be70-1 = ?
 
       cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → CC0 (h⁻¹ bx cc1 ) 
-      cc10 = ?
+      cc10 {x} bx (case1 x₁) = case1 ?
+      cc10 {x} bx (case2 x₁) = ?
 
       cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x) → CC1 (h ax cc0 ) 
-      cc11 = ?
+      cc11 {x} bx (case1 x₁) = case1 (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁)))
+      cc11 {x} bx (case2 x₁) = ?
+
+      be74 : (x : Ordinal) (ax : odef (* a) x) → odef (* b) (h ax (cc0 x))
+      be74 x ax with cc0 x
+      ... | case1 lt1 = ?
+      ... | case2 lt1 with iB be10 ? ?
+      ... | t = ?
+
+      be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx (cc1 x))
+      be75 x lt with cc1 x
+      ... | case1 lt1 = ?
+      ... | case2 lt1 = ?
 
       be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
       be72 x bx (case1 x₁)  with cc10 bx (case1 x₁)