# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565584139 -32400
# Node ID af60c40298a4edf8d77164fdfe2f2188470db0f7
# Parent  cb6f025a991ea700ad16ea70ab516eaa29554d1f
function continue

diff -r cb6f025a991e -r af60c40298a4 cardinal.agda
--- a/cardinal.agda	Mon Aug 12 08:59:55 2019 +0900
+++ b/cardinal.agda	Mon Aug 12 13:28:59 2019 +0900
@@ -24,28 +24,40 @@
 -- we have to work on Ordinal to keep OD Level n
 -- since we use p∨¬p which works only on Level n
 
-func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
-func→od f dom = Replace dom ( λ x →  x , (ord→od (f (od→ord x) )))
+<_,_> : (x y : OD) → OD
+< x , y > = (x , x ) , (x , y )
 
-record _⊗_  (A B : Ordinal) : Set n where
+record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where
    field
       π1 : Ordinal
       π2 : Ordinal
-      A∋π1 : def (ord→od A)  π1
-      B∋π2 : def (ord→od B)  π2
+      A∋π1 : def A π1
+      B∋π2 : def B π2
+      -- opair :  x ≡ od→ord (Ord ( omax (omax π1 π1)  (omax π1 π2) )) -- < π1 , π2 >
+
+open SetProduct
 
--- Clearly wrong. We need ordered pair
-Func :  ( A B : OD ) → OD
-Func A B = record { def = λ x → (od→ord A) ⊗ (od→ord B) }
+_⊗_  : (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 >) ) }
+
+--  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
 
-open  _⊗_
+Func :  ( A B : OD ) → OD
+Func A B = record { def = λ x → def (Power (A ⊗ B)) x } 
+
+-- 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} f lt x = sup-o ( λ y → lemma  y ) where
+func←od : { dom cod : OD } → {f : OD }  → Func dom cod ∋ f → (Ordinal → Ordinal )
+func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
    lemma : Ordinal → Ordinal
-   lemma y with p∨¬p ( _⊗_.π1 lt ≡ x )
-   lemma y | case1 refl = _⊗_.π2 lt
-   lemma y | case2 not = o∅
+   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
+
+func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
+func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
+
 
 -- contra position of sup-o<
 --
@@ -68,7 +80,7 @@
        ymap : Ordinal 
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od (ord→od xmap) xfunc ( func←od (ord→od ymap) yfunc y )  ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od  {!!} ( func←od  {!!} y )  ≡ y
 
 open Onto
 
@@ -88,7 +100,7 @@
        xfunc1 = {!!}
        zfunc : def (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od (ord→od xmap1) xfunc1 ( func←od (ord→od zmap) zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  {!!} ( func←od  zfunc z )  ≡ z
        onto-iso1   = {!!}