--- a/OPair.agda	Fri Jul 17 16:33:30 2020 +0900
+++ b/OPair.agda	Fri Jul 17 18:57:40 2020 +0900
@@ -136,36 +136,24 @@
 p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
+_⊗_ : (A B : HOD) → HOD
+A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
-_⊗_  : (A B : HOD) → HOD
-A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
-        odmax = pmax; <odmax = <pmax } where
+product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+product→ {A} {B} {a} {b} A∋a B∋b = {!!}
+
+record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p )  : Set (suc n) where
+  field
+    is-pair : def ZFProduct (od→ord p)
+    π1A : A ∋ π1 is-pair 
+    π2B : B ∋ π2 is-pair 
+
+product← : {A B a b p : HOD} → (lt : (A ⊗ B ) ∋ p )  → IsProduct A B p lt
+product← lt = record { is-pair = {!!} ; π1A = {!!} ; π2B = {!!} }
+
+ 
+ZFP  : (A B : HOD) → ( {x : HOD } → hod-ord< {x} ) → HOD
+ZFP  A B hod-ord< = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
+        odmax = {!!} ; <odmax = {!!} } where
     checkAB : { p : Ordinal } → def ZFProduct p → Set n
     checkAB (pair x y) = odef A x ∧ odef B y
-    pmax : Ordinal
-    pmax =  next (omax (od→ord A)  (od→ord B))
-    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< next (omax (od→ord A)  (od→ord B))
-    <pmax {y} prod = {!!} where
-         prod-odmax : ( x y : HOD) → Ordinal
-         prod-odmax x y = omax (od→ord (x , x)) (od→ord (x , y))
-         lemma : {x y z : HOD } → ((x , x ) , (x , y )) ∋ z → od→ord z o< osuc (osuc (od→ord (x , y) ))
-         lemma {x} {y} {z} = {!!}
-         lemma1 : {x y  : HOD } → A ∋ x → B ∋ y → od→ord (x , y) o< omax (odmax A) (odmax B)
-         lemma1 {x} {y} A∋x  B∋y with trio< (odmax A) (odmax B)
-         lemma1 {x} {y} A∋x B∋y | tri< a ¬b ¬c = begin
-                 od→ord (x , y)
-              ≤⟨ {!!} ⟩
-                 odmax B
-              ∎ where open o≤-Reasoning O
-         lemma1 {x} {y} A∋x B∋y | tri≈ ¬a b ¬c = {!!}
-         lemma1 {x} {y} A∋x B∋y | tri> ¬a ¬b c = {!!}
-
---            lemma2 : od→ord (x , y) o< osuc (omax (odmax A) (odmax B))
---            lemma2 = begin
---                 {!!}
---              ≤⟨ {!!} ⟩
---                 {!!}
---              ∎ where open o≤-Reasoning O
-         a = π1 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
-         b = π2 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
-