--- a/cardinal.agda	Thu Aug 29 16:18:37 2019 +0900
+++ b/cardinal.agda	Sun Jun 07 20:31:30 2020 +0900
@@ -5,6 +5,8 @@
 open import zf
 open import logic
 import OD 
+import ODC
+import OPair
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties 
@@ -16,6 +18,8 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open OPair O
+open ODAxiom odAxiom
 
 open _∧_
 open _∨_
@@ -24,50 +28,10 @@
 
 -- we have to work on Ordinal to keep OD Level n
 -- since we use p∨¬p which works only on Level n
---   < x , y > = (x , x) , (x , y)
-
-data ord-pair : (p : Ordinal) → Set n where
-   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
-
-ZFProduct : OD
-ZFProduct = record { def = λ x → ord-pair x }
-
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
--- eq-pair refl refl = HE.refl
-
-pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi1 ( pair x y) = x
-
-π1 : { p : OD } → ZFProduct ∋ p → Ordinal
-π1 lt = pi1 lt 
-
-pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi2 ( pair x y ) = y
-
-π2 : { p : OD } → ZFProduct ∋ p → Ordinal
-π2 lt = pi2 lt 
-
-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ ) 
-
-
-p-iso1 :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
-p-iso1 {ox} {oy} = pair ox oy
-
-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
-p-iso {x} p = ord≡→≡ (lemma p) where
-    lemma :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
-    lemma (pair ox oy) = refl
 
     
 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
-∋-p A x with p∨¬p ( A ∋ x )
+∋-p A x with ODC.p∨¬p O ( A ∋ x )
 ∋-p A x | case1 t = yes t
 ∋-p A x | case2 t = no t
 
@@ -88,7 +52,6 @@
 
 -- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
 
-
 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
 
@@ -98,17 +61,17 @@
       func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom
  
 od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {f} 
-od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } 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 = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
+   lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
            lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
-           lemma2 (pair x1 y1) with decp ( x1 ≡ x)
+           lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1
            lemma2 (pair x1 y1) | no ¬p = o∅
    fod : OD
-   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > )
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > )
 
 
 open Func←cd
@@ -139,7 +102,7 @@
 
 open Onto
 
-onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
+onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y  → Onto X Z
 onto-restrict {X} {Y} {Z} onto  Z⊆Y = record {
      xmap = xmap1
    ; ymap = zmap
@@ -167,15 +130,15 @@
 
 cardinal :  (X  : OD ) → Cardinal X
 cardinal  X = record {
-       cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
+       cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) )
      ; conto = onto
      ; cmax = cmax
    } where
     cardinal-p : (x  : Ordinal ) →  ( Ordinal  ∧ Dec (Onto X (Ord x) ) )
-    cardinal-p x with p∨¬p ( Onto X (Ord x)  ) 
+    cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x)  ) 
     cardinal-p x | case1 True  = record { proj1 = x  ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    S = sup-o (λ x → proj1 (cardinal-p x))
+    S = sup-o (λ x → proj1 (cardinal-p {!!}))
     lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
                     Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
     lemma1 x prev with trio< x (osuc S)
@@ -192,9 +155,9 @@
     ... | lift t = t <-osuc  
     cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) 
     cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
-       (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
+       (sup-o<  {λ x → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
-          lemma with  p∨¬p ( Onto X (Ord y) )
+          lemma with  ODC.p∨¬p O ( Onto X (Ord y) )
           lemma | case1 x = refl
           lemma | case2 not = ⊥-elim ( not ontoy )