# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566264997 -32400
# Node ID b6d80eec5f9e23f33978d153c26e70396a2ece37
# Parent  a8c6239176db2b0a863ad20b813c505f7b3ea3e2
...

diff -r a8c6239176db -r b6d80eec5f9e cardinal.agda
--- a/cardinal.agda	Mon Aug 19 11:39:46 2019 +0900
+++ b/cardinal.agda	Tue Aug 20 10:36:37 2019 +0900
@@ -33,13 +33,13 @@
 ZFProduct : OD
 ZFProduct = record { def = λ x → ord-pair x }
 
-π1' : { p : OD } → ZFProduct ∋ p → OD
-π1' lt = ord→od (pi1 lt) where
+π1 : { p : OD } → ZFProduct ∋ p → Ordinal
+π1 lt = pi1 lt where
    pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
    pi1 ( pair x y ) = x
 
-π2' : { p : OD } → ZFProduct ∋ p → OD
-π2' lt = ord→od (pi2 lt) where
+π2 : { p : OD } → ZFProduct ∋ p → Ordinal
+π2 lt = pi2 lt where
    pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
    pi2 ( pair x y ) = y
 
@@ -52,25 +52,15 @@
     ∎ )
     
 
-
-record SetProduct ( A B : OD )  : Set n where
-   field
-      π1 : Ordinal
-      π2 : Ordinal
-      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
-
 ∋-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  }
--- A ⊗ B  = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
+A ⊗ B  = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
+    checkAB : { p : Ordinal } → def ZFProduct p → Set n
+    checkAB (pair x y) = def A x ∧ def B y
 
 --  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
 
@@ -79,16 +69,6 @@
 
 -- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
 
-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
-   lemma : Ordinal → Ordinal
-   lemma 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 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)) > )
@@ -98,14 +78,25 @@
       func-1 : Ordinal → Ordinal
       func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
  
+od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f → (Ordinal → Ordinal )
+od→func {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
+   lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
+   lemma2 (pair x1 y1) with decp ( x1 ≡ x)
+   lemma2 (pair x1 y1) | yes p = y1
+   lemma2 (pair x1 y1) | no ¬p = o∅
+   lemma : Ordinal → Ordinal
+   lemma 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 y | p | no n  = o∅
+   lemma y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
+
 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
+   ... | t with decp ( x  ≡ π1 {!!} )
+   ... | yes _ = π2 {!!}
    ... | no _ = o∅
 
 func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
@@ -133,7 +124,7 @@
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
        onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
-          func←od {X} {Y} {xmap} xfunc ( func←od  yfunc y )  ≡ y
+          od→func {X} {Y} {xmap} xfunc ( od→func  yfunc y )  ≡ y
 
 open Onto
 
@@ -153,7 +144,7 @@
        xfunc1 = {!!}
        zfunc : def (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  xfunc1 ( func←od  zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → od→func  xfunc1 ( od→func  zfunc z )  ≡ z
        onto-iso1   = {!!}