--- a/cardinal.agda	Mon Aug 12 13:28:59 2019 +0900
+++ b/cardinal.agda	Tue Aug 13 22:21:10 2019 +0900
@@ -37,6 +37,11 @@
 
 open SetProduct
 
+∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+∋-p A x with p∨¬p ( A ∋ x )
+∋-p A x | case1 t = yes t
+∋-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 → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
@@ -48,12 +53,16 @@
 
 -- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
 
-func←od : { dom cod : OD } → {f : OD }  → Func dom cod ∋ f → (Ordinal → Ordinal )
+func←od : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f → (Ordinal → Ordinal )
 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
+   lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt
    lemma : Ordinal → Ordinal
-   lemma y with IsZF.power→ isZF (dom ⊗ cod) f lt
-   lemma y | p with double-neg-eilm ( p {ord→od y} {!!} ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
-   ... | t = π2 t
+   lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma y | p | no n  = o∅
+   lemma 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 : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
@@ -80,7 +89,8 @@
        ymap : Ordinal 
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od  {!!} ( func←od  {!!} y )  ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
+          func←od {X} {Y} {xmap} xfunc ( func←od  yfunc y )  ≡ y
 
 open Onto
 
@@ -100,7 +110,7 @@
        xfunc1 = {!!}
        zfunc : def (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  {!!} ( func←od  zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  xfunc1 ( func←od  zfunc z )  ≡ z
        onto-iso1   = {!!}