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

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

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

Func :  ( A B : HOD ) → OD
Func A B = record { def = λ x → (odef (Power (A ⊗ B)) x)
    ∧ ( (a b c : Ordinal) → odef (ord→od x) (od→ord < ord→od a , ord→od b >) ∧ odef (ord→od x) (od→ord < ord→od a , ord→od c >) →  b ≡  c ) }  

Func∋f : {A B x : HOD} → ( f : (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))) → (lt : A ∋ x ) → def (Func A B ) (od→ord  < x , proj1 (f x lt)  > )
Func∋f = {!!}

Func→f : {A B f x : HOD} → def ( Func A B) (od→ord f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
Func→f = {!!}

Func₁ : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}  
Func₁ = {!!}

Cod : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
Cod = {!!}

1-1 : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
1-1 = {!!}

onto : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
onto  = {!!}

record Bijection (A B : Ordinal ) : Set n where
   field
       bfun : Ordinal
       bfun-isfun : def (Func (ord→od A) (ord→od B))  bfun
       bfun-is1-1 : {!!}
       bfun-isonto : {!!}
       
Card : OD
Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }