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

diff -r b737a2e0b46e -r f464e48e18cc OPair.agda
--- a/OPair.agda	Thu Jul 30 21:45:49 2020 +0900
+++ b/OPair.agda	Fri Jul 31 11:21:27 2020 +0900
@@ -136,11 +136,12 @@
 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)))
 
-ω-pair : {x y : HOD} → infinite ∋ x → infinite ∋ y → od→ord < x , y > o< next o∅
-ω-pair {x} {y} lx ly = lemma0 where
-    lemma3 : od→ord (x , y) o< next o∅
-    lemma3 = next< (omax<nx (<odmax infinite lx) (<odmax infinite ly)) ho<
-    lemma0 : od→ord < x , y > o< next o∅
+ω-pair :  {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord (x , y) o< next m
+ω-pair lx ly = next< (omax<nx lx ly ) ho<
+
+ω-opair : {x y : HOD} → {m : Ordinal} → od→ord x o< next m → od→ord y o< next m → od→ord < x , y > o< next m
+ω-opair {x} {y} {m} lx ly = lemma0 where
+    lemma0 : od→ord < x , y > o< next m
     lemma0 = osucprev (begin
          osuc (od→ord < x , y >)
        <⟨ osuc<nx ho< ⟩
@@ -149,27 +150,54 @@
          next (osuc (od→ord (x , y)))
        ≡⟨ sym (nexto≡) ⟩
          next (od→ord (x , y))
-       ≤⟨ x<ny→≤next lemma3 ⟩
-         next o∅
+       ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
+         next m
        ∎ ) where
           open o≤-Reasoning O
 
 _⊗_ : (A B : HOD) → HOD
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
--- product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
--- product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (od→ord (Select (A ⊗ B) (λ x → x =h= < a , b >))) record { proj1 = {!!} ; proj2 = {!!} }
+product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (od→ord (Replace A (λ a → < a , b >)))
+             record { proj1 = lemma1 ; proj2 = subst (λ k → odef k (od→ord < a , b >)) (sym oiso) lemma2 } where
+    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (od→ord (Replace A (λ a₁ → < a₁ , b >)))
+    lemma1 = replacement← B b B∋b
+    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (od→ord < a , b >)
+    lemma2 = replacement← A a A∋a
+
+-- ⊗⊆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
+
+x<nextA : {A x : HOD} → A ∋ x →  od→ord x o< next (odmax A)
+x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
 
-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 
+A<Bnext : {A B x : HOD} → od→ord A o< od→ord B → A ∋ x → od→ord x o< next (odmax B)
+A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
+          osuc (od→ord x)  
+       <⟨ osucc (c<→o< A∋x) ⟩
+          osuc (od→ord A)
+       <⟨ osucc lt ⟩
+          osuc (od→ord B)
+       <⟨ osuc<nx ho<  ⟩
+          next (odmax B)
+       ∎ ) where open o≤-Reasoning O
 
--- product← : {A B a b p : HOD} → (lt : (A ⊗ B ) ∋ p )  → IsProduct A B p lt
--- product← {_} {_} {a} {b} lt = record { is-pair = {!!} ; π1A = {!!} ; π2B = {!!} }
+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 } 
+   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 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 = {!!}
 
- 
--- 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 (odmax A) (odmax B) ; <odmax = λ {y} px → {!!}  } -- (<odmax A (proj2 px (proj1 px) ))
diff -r b737a2e0b46e -r f464e48e18cc cardinal.agda
--- a/cardinal.agda	Thu Jul 30 21:45:49 2020 +0900
+++ b/cardinal.agda	Fri Jul 31 11:21:27 2020 +0900
@@ -54,9 +54,9 @@
 record Bijection (A B : Ordinal ) : Set n where
    field
        bfun : Ordinal
-       bfun-isfun : def (Func {!!} {!!} )  bfun
-       bfun-is1-1 : ?
-       bfun-isonto : ?
+       bfun-isfun : def (Func (ord→od A) (ord→od B))  bfun
+       bfun-is1-1 : {!!}
+       bfun-isonto : {!!}
        
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }