# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596167205 -32400
# Node ID f6f08d5a49410cea46855b6304a5a3915d51421e
# Parent  f464e48e18cc078f44d4a93c8f794603a92b9fe7
...

diff -r f464e48e18cc -r f6f08d5a4941 OPair.agda
--- a/OPair.agda	Fri Jul 31 11:21:27 2020 +0900
+++ b/OPair.agda	Fri Jul 31 12:46:45 2020 +0900
@@ -166,6 +166,7 @@
     lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >)
     lemma2 = replacement← A a A∋a
 
+-- axiom of choice required
 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (od→ord x)
 -- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (od→ord k )) {!!} op-cons
 
@@ -185,19 +186,35 @@
 
 ZFP  : (A B : HOD) → HOD
 ZFP  A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
-        odmax = omax (od→ord A) (od→ord B) ; <odmax = λ {y} px → lemma y px } 
+        odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px } 
    where
-       pp : { x y : Ordinal } → HOD
-       pp {x} {y} = (ord→od x , ord→od x) , (ord→od x , ord→od y)
-       lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (od→ord A) (od→ord B)
+       lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B))
        lemma y lt with proj1 lt
-       lemma p lt | pair x y with trio< (od→ord A) (od→ord B) | proj2 lt (pair x y)
-       lemma p lt | pair x y | tri< a ¬b ¬c | ab = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym diso)
-           (proj1 (proj2 lt (pair x y))))) (x<nextA {{!!}} {ord→od y} (proj2 lt))) (osucprev (  begin
-                     osuc (next (odmax B))
-                  ≤⟨ {!!}  ⟩
-                     osuc (od→ord B)
-                  ∎ )) where open o≤-Reasoning O
-       lemma p lt | pair x y | tri≈ ¬a b ¬c | ab = {!!}
-       lemma p lt | pair x y | tri> ¬a ¬b c | ab = {!!}
+       lemma p lt | pair x y with trio< (od→ord A) (od→ord B) 
+       lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym diso)
+           (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where
+               lemma1 : odef B y → od→ord (ord→od y) o< next (HOD.odmax B)
+               lemma1 lt = x<nextA {B} (d→∋ B lt)
+       lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where
+                lemma2 :  od→ord (ord→od y) o< next (HOD.odmax A)
+                lemma2 = ordtrans ( subst (λ k → od→ord (ord→od y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
+       lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
+           (A<Bnext c (subst (λ k → odef B k ) (sym diso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ ) 
 
+ZFP⊗ :  {A B : HOD} → ZFP A B ≡ A ⊗ B
+ZFP⊗ {A} {B} = ==→o≡ record { eq→ = lemma0 ; eq← = lemma1 } where
+      lemma0 :  {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
+      lemma0 {px} record { proj1 = (pair x y) ; proj2 = p2 } = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
+      lemma1 :  {x : Ordinal} → odef (A ⊗ B) x → odef (ZFP A B) x
+      lemma1 {x} lt = ⊥-elim (lt (λ u not → proj2 (proj1 not) (λ y p → lemma2 u y p ))) where
+           lemma2 : (u y : Ordinal) → odef B y ∧ (u ≡ od→ord (Replace A (λ a → < a , ord→od y >))) → ⊥
+           lemma2 = {!!}
+
+
+
+
+
+
+
+
+