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

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

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 (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⁻¹ = ?
            a∋g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → odef (* a) (g⁻¹ bx ) 
            a∋g⁻¹ = ?
            is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → x ≡ fab (g⁻¹ bx ) (a∋g⁻¹ bx)
            is-g⁻¹ = ?
            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 = g⁻¹ (b∋fab x ax)  
                    ; ay = subst (λ k → odef k ( g⁻¹ (b∋fab x ax))) (sym *iso) record { i = 0 ; gfix = a-g ? ? } ; x=fy = is-g⁻¹ ? }
                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
    be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ 
    be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥  } 
          ind a b a<b iab iba where
       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 = ?
    be00 : OrdBijection a b
    be00 with trio< a b
    ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )
    ... | tri≈ ¬a b ¬c = ordbij-refl b
    ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab )

_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 = {!!}