{-# OPTIONS --allow-unsolved-metas #-}

open import Level hiding (suc ; zero )
open import Ordinals
module cardinal {n : Level } (O : Ordinals {n}) where

open import logic
-- import OD
import OD hiding ( _⊆_ )

import ODC
open import Data.Nat 
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom
open import ZProduct O

import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
-- open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

_⊆_ : ( A B : HOD ) → Set n
_⊆_ A B = {x : Ordinal } → odef A x → odef B x


open _∧_
open _∨_
open Bool
open _==_

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
    }

open Injection
open OrdBijection

record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where
   field
      y : Ordinal 
      ay : odef (* a) y
      x=fy : x ≡ i→ iab _ ay

Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD
Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00  } where
    im00 : {x : Ordinal } → IsImage a b iab x → x o< b
    im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso 
         (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) )

record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where
   field
      y : Ordinal 
      ay : odef a y
      x=fy : x ≡ f y ay

record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where
   field
      ax : odef (* a) x
      x=fy : y ≡ i→ iab x ax

InverseImage : {a : Ordinal} ( b : Ordinal ) → Injection a b → (y : Ordinal ) → HOD
InverseImage {a} b iab y = record { od = record { def = λ x → IsInverseImage a b iab x y } ; odmax = & (* a) ; <odmax = im00  } where
    im00 : {x : Ordinal } → IsInverseImage a b iab x y → x o< & (* a)
    im00 {x} record { ax = ax ; x=fy = x=fy } = odef< ax

Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b 
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 )

c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?)
c=→≡ = ?

≡→c= : {A B : HOD} → A ≡ B → A =c= B
≡→c= = ?

open import BAlgebra O

_-_ : (a b : Ordinal ) → Ordinal 
a - b = & ( (* a) ＼ (* b) )

-→<  : (a b : Ordinal ) → (a - b) o≤ a
-→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) )

b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x
b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt
... | ⟪ bx , ¬ax ⟫ = bx

open Data.Nat

Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b
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  } 

Injection-∙ : {a b c : Ordinal } → Injection a b → Injection b c → Injection a c
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)   } 


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 (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 bx → be72 x bx (cc1 x) (cc0 (h⁻¹ bx (cc1 x)))
       ; fiso→ = λ x ax → be73 x ax (cc0 x) (cc1 (h ax (cc0 x)))
       }
 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 :  (x : Ordinal) → Set n where
          a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage  x
          next-gf : {x : Ordinal} → (ix : IsImage a a gf x) → (gfiy : gfImage (IsImage.y ix) ) → gfImage  x

      a∋gfImage : {x : Ordinal } → gfImage x → odef (* a) x
      a∋gfImage {x} (a-g ax ¬ib) = ax
      a∋gfImage  {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) )

      UC : HOD
      UC = record { od = record { def = λ x → gfImage x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage lt)  }

      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

      UC⊆a : * (& UC) ⊆ * a
      UC⊆a {x} lt = a∋gfImage  be02  where
            be02 : gfImage x
            be02 = subst (λ k → odef k x) *iso lt

      a-UC⊆a : * (& a-UC) ⊆ * a
      a-UC⊆a {x} lt = proj1 ( subst (λ k → odef k x) *iso lt )

      open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )

      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 ))  

      UC∋gf : {y : Ordinal } → (uy : odef (* (& UC)) y ) → gfImage ( fba (fab y (UC⊆a uy) ) (b∋fab y  (UC⊆a uy)))
      UC∋gf {y} uy = next-gf record { y = _ ; ay = UC⊆a uy ; x=fy = fba-eq (fab-eq refl) }  uc00  where
          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 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 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 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} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) 

      g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a g x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0'
      g⁻¹-eq {x} ax ax' {record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ }} {record { y = y ; ay = ay ; x=fy = x=fy }} 
           = inject g _ _ ay₁ ay (trans (sym x=fy₁) x=fy )

      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 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))
      cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } with nimg ax ncn
      ... | record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } = ncn ( subst (λ k → gfImage k) be113 
                                            (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) )  where
               be113 : fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡ x
               be113 = begin
                    fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡⟨ fba-eq (sym x=fy)  ⟩
                    fba y1 ay1 ≡⟨ sym (x=fy1) ⟩
                    x ∎ where open ≡-Reasoning

      be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x
      be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = be18 } where
          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
              be14 : odef a-UC x 
              be14 = subst (λ k → odef k x) *iso lt
              be19 : odef (* b) (g⁻¹ (be15 lt) (be16 lt))
              be19 = b∋g⁻¹ (be15 lt) (be16 lt)
              be18 : odef a-UC x →  ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 lt) (be16 lt))
              be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be113 (UC∋gf ay) ) where
                   be113 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x
                   be113 = begin
                      fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy)  ⟩
                      fba (g⁻¹ (be15 lt) (be16 lt)) be19 ≡⟨ g⁻¹-iso (be15 lt) (be16 lt) ⟩
                      x ∎ where open ≡-Reasoning
          be18 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → g⁻¹ (be15 ltx) (be16 ltx) ≡ g⁻¹ (be15 lty) (be16 lty) → x ≡ y
          be18 = ?

      be13 : (x : Ordinal) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal
      be13 x lt = fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt ))

      be60 : {b x : Ordinal} → (bx : odef (* b) x) → (ncn : ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) ) 
           → odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
      be60 {b} {x} bx ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫

      cc10-case2 : {x : Ordinal } → (bx : odef (* b) x )
         → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax))  x
         → ¬ gfImage (fba x bx)
      cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl }
      cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) 
           = nix record { y = _ ; ay = gfy ; x=fy = inject g _ _ bx (b∋fab y (a∋gfImage gfy)) (trans x=fy (fba-eq (fab-eq refl))) }

      be11 : Injection  (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC)   -- g x
      be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where
          be14 : (x : Ordinal) (lt : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& a-UC)) (be13 x lt)
          be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be25 ⟫ where
              be26 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x)
              be26 = proj2 ( subst (λ k → odef k x) (*iso) lt )
              be25 : ¬ gfImage (be13 x lt)
              be25 cn with cn
              ... | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } )
              ... | next-gf  record { y = y ; ay = ay ; x=fy = x=fy } t 
                   = ⊥-elim (be26 (subst (λ k → odef k x) (sym *iso) record { y = y 
                      ; ay = subst (λ k → odef k y) (sym *iso) t ; x=fy = be17 })) where
                  be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) t))
                  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 )) (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 ))) )
      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy )
      ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl })

      a-UC-iso11 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) 
           → (ib : odef (* (& a-UC)) (fba x ( proj1 ( subst (λ k → odef k x) (*iso) cx )) ))
           → i→ be10 ( i→ be11 x cx ) ib  ≡ x
      a-UC-iso11 x cx ib with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) )
      ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy )
      ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl })

      --   C n → f (C n) 
      fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal
      fU x lt = be03 where
            be02 : gfImage x
            be02 = subst (λ k → odef k x) *iso lt
            be03 : Ordinal
            be03 with be02
            ... | a-g {x} ax ¬ib = fab x ax
            ... | 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) ))

      fU1 : (x : Ordinal) → odef UC x → Ordinal
      fU1 x gfx = fab x (a∋gfImage gfx)

      --   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

      b∋Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x
      b∋Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋fab y (a∋gfImage ay))

      Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal
      Uf1 x lt = fba x (b∋Uf1 x lt) 

      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 : gfImage x
            be02 = subst (λ k → odef k x) *iso cx
            be06 :  odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx)
            be06 with be02
            ... | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-eq refl } 
            ... | 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 : gfImage x
            be02 = subst (λ k → odef k x) *iso cx
            be03 : Uf ( fU x cx ) (be04 cx)  ≡ x
            be03 with be02 | be04 cx
            ... | 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 | 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) )

      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 subst (λ k → OD.def (od k) y) *iso ay
            ... | a-g ax ¬ib = sym x=fy
            ... | next-gf t ix = sym x=fy

      UC-iso11 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f)))) x ) 
         → (ux : odef (* (& UC)) (Uf x cx)) → fU ( Uf x cx ) ux  ≡ x
      UC-iso11 x cx ux = subst (λ k → fU (Uf x cx) k ≡ x) ( HE.≅-to-≡ ( ∋-irr {* (& UC)} {_} (be08 cx) ux)) (UC-iso1 x cx)

      CC0 : (x : Ordinal) → Set n
      CC0 x =  gfImage x ∨ (¬ gfImage x) 

      CC1 : (x : Ordinal) → Set n
      CC1 x =  IsImage0 UC (* b) FA x ∨  (¬ IsImage0 UC (* b) FA x) 

      cc0 : (x : Ordinal) → CC0 x 
      cc0 x = ODC.p∨¬p O (gfImage x) 

      cc1 : (x : Ordinal) → CC1 x 
      cc1 x = ODC.p∨¬p O (IsImage0 UC (* b) FA x) 

      cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) 
      cc20 {x} lt = cc0 (fba x lt)

      cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) 
      cc21 {x} lt = cc1 (fab 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
      --  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) → CC0 x → Ordinal
      h {x} ax (case1 cn)  = fU1 x cn
      h {x} ax (case2 ncn) = g⁻¹ ax (nimg ax ncn)

      h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → CC1 x → Ordinal
      h⁻¹ {x} bx ( case1 cn)  = Uf1 x cn                    --   x ≡ f y
      h⁻¹ {x} bx ( case2 ncn) = fba x bx

      cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x ) → CC0 (h⁻¹ bx cc1 ) 
      cc10 {x} bx (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = 
          case1 (next-gf record { y = _ ; ay = a∋gfImage ay ; x=fy = fba-eq x=fy } ay )
      cc10 {x} bx (case2 x₁) = case2 (cc10-case2 bx x₁ ) 

      cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ) → CC1 (h ax cc0 ) 
      cc11 {x} ax (case1 x₁) = case1 record {y = _ ; ay = x₁ ; x=fy = refl } 
      cc11 {x} ax (case2 x₁) = case2 (cc11-case2 ax x₁)

      be70 : (x : Ordinal) (lt : odef (* a) x) → (or :  CC0 x ) → odef (* b) (h lt or )
      be70 x ax ( case1 cn ) = b∋fab x (a∋gfImage cn)
      be70 x ax ( case2 ncn ) = b∋g⁻¹ ax (nimg ax ncn)

      be71 :  (x : Ordinal) (bx : odef (* b) x) → (or : CC1 x) → odef (* a) (h⁻¹ bx or )
      be71  x bx ( case1 cn ) = subst (λ k → odef (* a) k) (fba-eq refl) (a∋fba x bx  )
      be71 x bx ( case2 ncn ) = a∋fba x bx 

      be71-1 :  (x : Ordinal) (bx : odef (* b) x) 
             → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) 
             → gfImage (h⁻¹ bx (case1 ? ) )
      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 = ?

      be74 : (x : Ordinal) (ax : odef (* a) x) (cc0 : CC0 x) → odef (* b) (h ax cc0 )
      be74 x ax with cc0 
      ... | t = ?

      be75 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) → odef (* a) (h⁻¹ bx cc1 )
      be75 x lt  = ?

      fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx)
      fba-image {x} bx = record { y = _ ; ay = bx ; x=fy = refl }

      ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
      ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))

      be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x ) (cc0 : CC0 (h⁻¹ bx cc1)) →  h (be75 x bx cc1) cc0 ≡ x
      be72 x bx (case1 x₁) t = ?
      be72 x bx (case2 x₁) t = ?


      be73 :  (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) (cc1 : CC1 (h ax cc0)) →  h⁻¹ (be74 x ax cc0) cc1  ≡ x
      be73 x ax (case1 x₁) t = ?
      be73 x ax (case2 x₁) t = ?


_c<_ : ( A B : HOD ) → Set n
A c< B = ¬ ( Injection (& A)  (& B) )

Card : OD
Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection 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

Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s →   s c< Ord t
Cardinal∈ = {!!}

Cardinal⊆ : { s t : HOD } → s ⊆ t →  ( s c< t ) ∨ ( s =c= t )
Cardinal⊆ = {!!}

Cantor1 : { u : HOD } → u c< Power u
Cantor1 = {!!}

Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
Cantor2 = {!!}