--- a/cardinal.agda	Mon Aug 19 00:37:35 2019 +0900
+++ b/cardinal.agda	Mon Aug 19 11:39:46 2019 +0900
@@ -27,32 +27,31 @@
 <_,_> : (x y : OD) → OD
 < x , y > = (x , x ) , (x , y )
 
-Ord< : {x y : Ordinal } → x o< y  → od→ord (Ord x) o< od→ord (Ord y)  -- x o< y = Ord y ∋ x → ox o< od→ord (Ord y) 
-Ord< {x} {y} lt with trio< (od→ord (Ord x)) (od→ord (Ord y))
-Ord< {x} {y} lt | tri< a ¬b ¬c =  a        
-Ord< {x} {y} lt | tri≈ ¬a b ¬c =  ⊥-elim ( o<¬≡ refl (def-subst {Ord y} {x} {Ord x} {x} lt   -- Ord x ∋ x
-    (subst₂ (λ j k → j ≡ k) oiso oiso (cong (λ k → ord→od k )(sym b)) )refl ))               -- Ord x ≡ Ord y
-Ord< {x} {y} lt | tri> ¬a ¬b c =  ? where
-     lemma : ¬ ( Ord x ∋ ord→od x )
-     lemma lt = ⊥-elim ( o<¬≡ refl ( def-subst {_} {_} {Ord x} {x} lt refl diso )) 
-     lemma1 : od→ord (Ord y) o< od→ord (Ord x) → x o< od→ord (Ord x )
-     lemma1 lt1 = ordtrans ( o<-subst (c<→o< lt ) diso refl ) {!!} 
+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 }
+
+π1' : { p : OD } → ZFProduct ∋ p → OD
+π1' lt = ord→od (pi1 lt) where
+   pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+   pi1 ( pair x y ) = x
 
----   Ord (osuc ox) ∋ x
----   ox o< od→ord (Ord (osuc ox)) 
----   osuc ox  ≡ od→ord (Ord (osuc ox)) 
+π2' : { p : OD } → ZFProduct ∋ p → OD
+π2' lt = ord→od (pi2 lt) where
+   pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+   pi2 ( pair x y ) = y
 
-opair : {x y : OD} → ( < x , y > ∋ x ) ∧ ( < x , y > ∋ y )
-opair {x} {y} = record { proj1 = lemma ; proj2 = {!!} } where
-   ox = (od→ord x)
-   oy = (od→ord y)
-   -- < x , y > ∋ x  --  od→ord (Ord (omax ox ox ))
-   lemma : ox o< (omax (od→ord (x , x)) (od→ord (x , y)))
-   lemma with trio< ox oy
-   lemma | tri< a ¬b ¬c with omax< ox oy a | omxx ox
-   ... | eq | eq1 = {!!}
-   lemma | tri≈ ¬a b ¬c = {!!}
-   lemma | tri> ¬a ¬b c = {!!}
+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 >
+    ∎ )
+    
+
 
 record SetProduct ( A B : OD )  : Set n where
    field