open import Level
open import Ordinals
module cardinal {n : Level } (O : Ordinals {n}) where

open import zf
open import logic
import OD 
import ODC
import OPair
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
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 OPair O
open ODAxiom odAxiom

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


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

open HOD

-- _⊗_ : (A B : HOD) → HOD
-- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))

Func :  OD
Func = record { def = λ x → def ZFProduct x
    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }  

FuncP :  ( A B : HOD ) → HOD
FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) } 
       ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }

Func∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
    → def Func (&  (Replace A (λ x → < x , f x > )))
Func∋f = {!!}

FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
    → odef (FuncP A B) (&  (Replace A (λ x → < x , f x > )))
FuncP∋f = {!!}

-- Func→f : {A B f x : HOD} → def Func (& f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
-- Func→f = {!!}
-- Func₁ : {A B f : HOD} → def Func (& f) → {!!}  
-- Func₁ = {!!}
-- Cod : {A B f : HOD} → def Func (& f) → {!!}
-- Cod = {!!}
-- 1-1 : {A B f : HOD} → def Func (& f) → {!!}
-- 1-1 = {!!}
-- onto : {A B f : HOD} → def Func (& f) → {!!}
-- onto  = {!!}

record Bijection (A B : Ordinal ) : Set n where
   field
       fun→ : Ordinal → Ordinal
       fun← : Ordinal → Ordinal
       fun→inA : (x : Ordinal) → odef (* A) ( fun→ x )
       fun←inB : (x : Ordinal) → odef (* B) ( fun← x )
       fiso→ : (x : Ordinal ) → odef (* B)  x → fun→ ( fun← x ) ≡ x
       fiso← : (x : Ordinal ) → odef (* A)  x → fun← ( fun→ x ) ≡ x
       
Card : OD
Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }