--- a/src/cardinal.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/cardinal.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -45,14 +45,28 @@
 -- _⊗_ : (A B : HOD) → HOD
 -- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
-Func :  OD
-Func = record { def = λ x → def ZFPair x
-    ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }
+record Func (A B : HOD) : Set n where
+    field
+       func : Ordinal → Ordinal
+       is-func : {x : Ordinal } → odef A x → odef B (func x)
+
+data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace A ( λ x → < x , (* (Func.func F (& x))) > )))
+
+FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
+FuncHOD→F {A} {B} (felm F) = F
 
-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 ? ≡ pi1 ? → pi2 ? ≡ pi2 ? ) }
-       ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
+FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace A ( λ x → < x , (* (Func.func (FuncHOD→F fc) (& x))) > )
+FuncHOD=R {A} {B}  (felm F) = *iso
+
+Funcs : (A B : HOD) → HOD
+Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (A ⊗ B)) 
+       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (A ⊗ B)) ) &iso (⊆→o≤ (lemma1 px)) } where
+    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (A ⊗ B) x
+    lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
+    ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (A ⊗ B) k ) (sym x=ψz) (
+       product→ (subst (λ k → odef A k) (sym &iso) az) (subst (λ k → odef B k) 
+         (trans (cong (Func.func F) (sym &iso)) (sym &iso)) (Func.is-func F az) ))
 
 record Injection (A B : Ordinal ) : Set n where
    field