--- a/cardinal.agda	Wed Aug 28 20:32:35 2019 +0900
+++ b/cardinal.agda	Wed Aug 28 23:52:54 2019 +0900
@@ -88,6 +88,7 @@
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
     ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
 
+
 data ord-pair : (p : Ordinal) → Set n where
    pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
 
@@ -118,20 +119,35 @@
     ∎ )
 
 
-p-iso-1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x
-p-iso-1 {x} {y} p  = lemma1 {od→ord < x , y >} {od→ord x} {od→ord y} p (cong₂ (λ j k → ord-pair (od→ord < j , k >)) (sym oiso) (sym oiso) ) where
-    lemma1 : {op ox oy : Ordinal } → ( p : ord-pair op ) → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > )) → pi1 p ≡ ox
-    lemma1 (pair ox oy) eq = {!!}
-    lemma2 : {op ox oy : Ordinal } →  ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > ))
-    lemma2 = {!!}
-    lemma0 : {op ox oy : Ordinal } → ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )))  → pi1 p ≡ ox
-    lemma0 = {!!}
-    lemma3 : {ox oy : Ordinal } ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )) ) →   pi1 p  ≡ ox
-    lemma3 {ox} {oy} p = {!!}
-    lemma4 : {ox oy : Ordinal }   →  ord-pair (od→ord < ord→od ox , ord→od oy > ) ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
-    lemma4  = refl
-    lemma : {p : OD }  →  ord-pair (od→ord p) ≡ ZFProduct ∋ p
-    lemma  = refl
+lemma44 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >)
+lemma44 {ox} {oy} = pair ox oy
+
+lemma55 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
+lemma55 {ox} {oy} = pair ox oy
+
+lemma66 : {ox oy : Ordinal } →  pair ( pi1 ( pair ox oy )) ( pi2 ( pair ox oy )) ≡ pair ox oy
+lemma66  = refl 
+
+lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy ))  , ord→od (pi2 ( pair ox oy ))  >  ≡ ZFProduct ∋ < ord→od ox , ord→od oy > 
+lemma77  = refl
+
+p-iso3 : { ox oy  : Ordinal } →  (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy
+p-iso3 p = {!!} where
+     lemma0 : {ox oy  : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
+     lemma0 = refl
+     lemma1 : {op ox oy : Ordinal } → op ≡ od→ord < ord→od ox , ord→od oy >  → ord-pair op ≡ ZFProduct ∋ < ord→od ox , ord→od oy >
+     lemma1 refl = refl
+     lemma : {op ox oy : Ordinal } → (p : ord-pair op ) →  od→ord < ord→od ox , ord→od oy > ≡ op → p ≅ pair ox oy
+     lemma {op} {ox} {oy} (pair ox' oy') eq = {!!}
+
+
+p-iso2 :  { ox oy  : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy
+p-iso2 = subst₂ ( λ j k → j ≡ k ) {!!} {!!} refl
+
+p-iso1 :  { x y  : OD } → (p : ZFProduct ∋ < x , y > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡  < x , y >
+p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p))
+... | t = {!!}
+    
 
 p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
 p-iso {x} p  = {!!}