--- a/cardinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/cardinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -27,7 +27,7 @@
 <_,_> : (x y : OD) → OD
 < x , y > = (x , x ) , (x , y )
 
-record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where
+record SetProduct ( A B : OD )  : Set n where
    field
       π1 : Ordinal
       π2 : Ordinal
@@ -43,7 +43,7 @@
 ∋-p A x | case2 t = no t
 
 _⊗_  : (A B : OD) → OD
-A ⊗ B  = record { def = λ x → SetProduct A B x }
+A ⊗ B  = record { def = λ x → SetProduct A B  }
 -- A ⊗ B  = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
 
 --  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
@@ -63,9 +63,27 @@
    ... | yes _ = π2 t
    ... | no _ = o∅
 
+
 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
 
+record Func←cd { dom cod : OD } {f : Ordinal } (f<F :  def (Func dom cod ) f) : Set n where
+   field
+      func-1 : Ordinal → Ordinal
+      func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
+ 
+func←od1 : { dom cod : OD } → {f : Ordinal }  → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
+func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
+   lemma : Ordinal → Ordinal → Ordinal
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y | p | no n  = o∅
+   lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
+   ... | t with decp ( x  ≡ π1 t )
+   ... | yes _ = π2 t
+   ... | no _ = o∅
+
+func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
+func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} }
 
 -- contra position of sup-o<
 --