--- a/OD.agda	Thu Aug 29 16:17:02 2019 +0900
+++ b/OD.agda	Fri Aug 30 15:37:04 2019 +0900
@@ -235,13 +235,59 @@
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
     ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
 
-ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
-ppp  {p} {a} d = d
+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 → OD
+π1 lt = ord→od (pi1 lt )
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : OD } → ZFProduct ∋ p → OD
+π2 lt = ord→od (pi2 lt )
+
+op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
+op-cons {ox} {oy} = pair ox oy
+
+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 >
+    ∎ ) 
+
+op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
+op-iso (pair ox oy) = refl
+
+p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
+p-iso {x} p = ord≡→≡ (op-iso p) 
+
+p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
+p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
+
+p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
+p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
 --
 -- Axiom of choice in intutionistic logic implies the exclude middle
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
+
+ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
+ppp  {p} {a} d = d
+
 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
 p∨¬p  p | yes eq = case2 (¬p eq) where
@@ -299,20 +345,6 @@
     ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
    } 
 
--- Constructible Set on α
--- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
--- L (Φ 0) = Φ
--- L (OSuc lv n) = { Def ( L n )  } 
--- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) )
--- L : {n : Level} → (α : Ordinal ) → OD 
--- L   record { lv = Zero ; ord = (Φ .0) } = od∅
--- L   record { lv = lx ; ord = (OSuc lv ox) } = Def ( L  ( record { lv = lx ; ord = ox } ) ) 
--- L   record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
---     cseq ( Ord (od→ord (L   (record { lv = lx ; ord = Φ lx }))))
-
--- L0 :  {n : Level} → (α : Ordinal ) → L (osuc α) ∋ L α
--- L1 :  {n : Level} → (α β : Ordinal ) → α o< β → ∀ (x : OD )  → L α ∋ x → L β ∋ x 
-
 OD→ZF : ZF  
 OD→ZF   = record { 
     ZFSet = OD 
@@ -382,10 +414,6 @@
          pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
          pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
 
-         -- pair0 : (A B : OD  ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         -- proj1 (pair A B ) = omax-x  (od→ord A) (od→ord B)
-         -- proj2 (pair A B ) = omax-y  (od→ord A) (od→ord B)
-
          empty : (x : OD  ) → ¬  (od∅ ∋ x)
          empty x = ¬x<0 
 

--- a/cardinal.agda	Thu Aug 29 16:17:02 2019 +0900
+++ b/cardinal.agda	Fri Aug 30 15:37:04 2019 +0900
@@ -24,46 +24,6 @@
 
 -- 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 )