# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688261737 -32400
# Node ID 52853b81df80555045dfdcb84df588f1235d9be0
# Parent  ea470857db440b55f737dc8f0bfc00814dc8dded
...

diff -r ea470857db44 -r 52853b81df80 src/cardinal.agda
--- a/src/cardinal.agda	Sun Jul 02 01:43:36 2023 +0900
+++ b/src/cardinal.agda	Sun Jul 02 10:35:37 2023 +0900
@@ -42,27 +42,27 @@
 
 open HOD
 
-record OrdBijection (A B : Ordinal ) : Set n where
-   field
-       fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
-       fun→  : (x : Ordinal ) → odef (* B)  x → Ordinal
-       funB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( fun← x lt )
-       funA  : (x : Ordinal ) → ( lt : odef (* B)  x ) → odef (* A) ( fun→ x lt )
-       fiso← : (x : Ordinal ) → ( lt : odef (* B)  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
-       fiso→ : (x : Ordinal ) → ( lt : odef (* A)  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
-
-ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
-ordbij-refl {a} refl = record {
-       fun←  = λ x _ → x 
-     ; fun→  = λ x _ → x 
-     ; funB  = λ x lt → lt
-     ; funA  = λ x lt → lt
-     ; fiso← = λ x lt → refl
-     ; fiso→ = λ x lt → refl
-    }
+-- record HODBijection (A B : HOD ) : Set n where
+--   field
+--       fun←  : (x : Ordinal ) → odef A  x → Ordinal
+--       fun→  : (x : Ordinal ) → odef B  x → Ordinal
+--       funB  : (x : Ordinal ) → ( lt : odef A  x ) → odef B ( fun← x lt )
+--       funA  : (x : Ordinal ) → ( lt : odef B  x ) → odef A ( fun→ x lt )
+--       fiso← : (x : Ordinal ) → ( lt : odef B  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
+--       fiso→ : (x : Ordinal ) → ( lt : odef A  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
+-- 
+-- rrdbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
+-- rrdbij-refl {a} refl = record {
+--       fun←  = λ x _ → x 
+--     ; fun→  = λ x _ → x 
+--     ; funB  = λ x lt → lt
+--     ; funA  = λ x lt → lt
+--     ; fiso← = λ x lt → refl
+--     ; fiso→ = λ x lt → refl
+--    }
 
 open Injection
-open OrdBijection
+open HODBijection
 
 record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
    field
@@ -96,7 +96,7 @@
 Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay)
 
 _=c=_ : ( A B : HOD ) → Set n
-A =c= B = OrdBijection ( & A ) ( & B )
+A =c= B = HODBijection A B 
 
 c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
 c=→≡ = ?
@@ -126,17 +126,41 @@
 Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax)
         ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq)   } 
 
+Exclusive : (A C : HOD) → Set n
+Exclusive A C = ({x : Ordinal} → odef A x → ¬ odef C x) ∧ ({x : Ordinal} → odef C x → ¬ odef A x)
 
-Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b
+bi-∪  : {A B C D : HOD } → (ab : HODBijection A B) → (cd : HODBijection C D )  
+       → HODBijection (A ∪ C) (B ∪ D)
+bi-∪  {A} {B} {C} {D} ab cd = record { 
+         fun←  = fa
+       ; fun→  = fb
+       ; funB  = fa-isb
+       ; funA  = fb-isa
+       ; fiso← = faiso
+       ; fiso→ = fbiso
+       } where
+          fa : (x : Ordinal) → odef (A ∪ C) x → Ordinal
+          fa x (case1 a) = fun← ab x a
+          fa x (case2 c) = fun← cd x c
+          fb : (x : Ordinal) → odef (B ∪ D) x → Ordinal
+          fb x (case1 b) = fun→ ab x b
+          fb x (case2 d) = fun→ cd x d
+          fa-isb :  (x : Ordinal) (lt : odef (A ∪ C) x) → odef (B ∪ D) (fa x lt)
+          fa-isb x (case1 a) = case1 (funB ab x a)
+          fa-isb x (case2 c) = case2 (funB cd x c)
+          fb-isa :  (x : Ordinal) (lt : odef (B ∪ D) x) → odef (A ∪ C) (fb x lt)
+          fb-isa x (case1 b) = case1 (funA ab x b)
+          fb-isa x (case2 d) = case2 (funA cd x d)
+          faiso : (x : Ordinal) (lt : odef (B ∪ D) x) → fa (fb x lt) (fb-isa x lt) ≡ x
+          faiso x (case1 b) = fiso← ab x b
+          faiso x (case2 d) = fiso← cd x d
+          fbiso : (x : Ordinal) (lt : odef (A ∪ C) x) → fb (fa x lt) (fa-isb x lt) ≡ x
+          fbiso x (case1 b) = fiso→ ab x b
+          fbiso x (case2 d) = fiso→ cd x d
+
+Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* 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 (cc0 x)
-       ; fun→  = λ x lt → h⁻¹ lt (cc1 x)
-       ; funB  = λ x lt → be74 x lt (cc0 x)
-       ; funA  = λ x lt → be75 x lt (cc1 x)
-       ; fiso← = λ x lt → be72 x lt (cc1 x)
-       ; fiso→ = λ x lt → be73 x lt (cc0 x)
-       }
+     = subst₂ (λ j k → HODBijection j k ) (sym a=UC∨a-UC) (sym b=fUC∨b-fUC) (bi-∪  bi-UC  bi-fUC)
  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) 
@@ -157,6 +181,35 @@
       a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ gfImage x) } ; odmax = & (* a) 
           ; <odmax = λ lt → odef< (proj1 lt)  }
 
+      a=UC∨a-UC : * a ≡ UC ∪ a-UC
+      a=UC∨a-UC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where
+           be00 : {x : Ordinal} → odef (* a) x → odef (UC ∪ a-UC) x
+           be00 {x} ax with ODC.p∨¬p O ( gfImage x)
+           ... | case1 gfx = case1 gfx
+           ... | case2 ngfx = case2 ⟪ ax , ngfx ⟫
+           be01 : {x : Ordinal} → odef (UC ∪ a-UC) x → odef (* a) x 
+           be01 {x} (case1 gfx) = a∋gfImage gfx
+           be01 {x} (case2 ngfx) = proj1 ngfx
+
+      FA : (x : Ordinal) → (ax : gfImage x) → Ordinal
+      FA x ax = fab x (a∋gfImage ax)
+
+      fUC : HOD
+      fUC = record { od = record { def = λ x → IsImage0 UC (* b) FA  x } ; odmax = & (* a) ; <odmax = λ lt → ? }
+
+      b-fUC : HOD
+      b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA  x) } ; odmax = & (* a) ; <odmax = λ lt → ? }
+
+      b=fUC∨b-fUC : * b ≡ fUC ∪ b-fUC
+      b=fUC∨b-fUC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where
+           be00 : {x : Ordinal} → odef (* b) x → odef (fUC ∪ b-fUC) x
+           be00 {x} bx with ODC.p∨¬p O (IsImage0 UC (* b) FA  x)
+           ... | case1 gfx = case1 gfx
+           ... | case2 ngfx = case2 ⟪ bx , ngfx ⟫
+           be01 : {x : Ordinal} → odef (fUC ∪ b-fUC) x → odef (* b) x 
+           be01 {x} (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* b) k) (sym x=fy) ( b∋fab y (a∋gfImage ay))
+           be01 {x} (case2 ngfx) = proj1 ngfx
+
       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
@@ -215,9 +268,6 @@
       be16 {x} lt with subst (λ k → odef k x) *iso lt
       ... | ⟪ ax , ncn ⟫ = nimg ax ncn
 
-      FA : (x : Ordinal) → (ax : gfImage x) → Ordinal
-      FA x ax = fab x (a∋gfImage ax)
-
       cc11-case2 : {x : Ordinal} (ax : odef (* a) x) 
           → (ncn : ¬ gfImage x) 
           → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax))  (g⁻¹ ax (nimg ax ncn))
@@ -376,13 +426,33 @@
       cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) 
       cc21 {x} lt = cc1 (fab x lt)
 
+      bi-UC : HODBijection UC fUC
+      bi-UC = record { 
+         fun←  = λ x lt → fU1 x lt
+       ; fun→  = λ x lt → Uf1 x lt
+       ; funB  = λ x lt → ?
+       ; funA  = λ x lt → ?
+       ; fiso← = λ x lt → ?
+       ; fiso→ = λ x lt → ?
+       }
+
+      bi-fUC : HODBijection a-UC b-fUC
+      bi-fUC = record { 
+         fun←  = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))
+       ; fun→  = λ x lt → fba x (proj1 lt)
+       ; funB  = λ x lt → ?
+       ; funA  = λ x lt → ?
+       ; fiso← = λ x lt → ?
+       ; fiso→ = λ x lt → ?
+       }
+
       --
       --  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
+      --     in HODBijection record, LEM rules are used
       --  but we cannot use LEM in second function call on iso parts.
       --  so we have to do some devices.
       --
@@ -448,13 +518,13 @@
 A c< B = ¬ ( Injection (& A)  (& B) )
 
 Card : OD
-Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x }
+Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ HODBijection (* a) (* x) }
 
 record Cardinal (a : Ordinal ) : Set (Level.suc n) where
    field
        card : Ordinal
-       ciso : OrdBijection a card
-       cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x
+       ciso : HODBijection (* a) (* card)
+       cmax : (x : Ordinal) → card o< x → ¬ HODBijection (* a) (* x)
 
 Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
 Cardinal∈ = {!!}