--- a/cardinal.agda	Fri Jul 31 12:57:59 2020 +0900
+++ b/cardinal.agda	Fri Jul 31 17:42:25 2020 +0900
@@ -26,37 +26,51 @@
 open Bool
 open _==_
 
+open HOD
+
 -- _⊗_ : (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)
+Func :  OD
+Func = record { def = λ x → def ZFProduct 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)  > )
+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 (od→ord  (Replace A (λ x → < x , f x > )))
 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 ))
+FuncP∋f : {A B x : HOD} → ( f : HOD → HOD ) → ( (x : HOD ) → A ∋ x → B ∋ f x )
+    → odef (FuncP A B) (od→ord  (Replace A (λ x → < x , f x > )))
+FuncP∋f = {!!}
+
+Func→f : {A B f x : HOD} → def Func (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₁ : {A B f : HOD} → def Func (od→ord f) → {!!}  
 Func₁ = {!!}
 
-Cod : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
+Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
 Cod = {!!}
 
-1-1 : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
+1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
 1-1 = {!!}
 
-onto : {A B f : HOD} → def ( Func A B) (od→ord f) → {!!}
+onto : {A B f : HOD} → def Func (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 : {!!}
+       fun→ : Ordinal → Ordinal
+       fun← : Ordinal → Ordinal
+       fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
+       fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x )
+       fiso→ : (x : Ordinal ) → odef (ord→od A)  x → fun→ ( fun← x ) ≡ x
+       fiso← : (x : Ordinal ) → odef (ord→od B)  x → fun← ( fun→ x ) ≡ x
        
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }