# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595994125 -32400
# Node ID 6dcea4c7cba1615fcc24737bae3330083eeb4aba
# Parent  3fba5f805e50ca628944ab81233f2ea4b413badb
...

diff -r 3fba5f805e50 -r 6dcea4c7cba1 OPair.agda
--- a/OPair.agda	Wed Jul 29 00:25:07 2020 +0900
+++ b/OPair.agda	Wed Jul 29 12:42:05 2020 +0900
@@ -49,19 +49,20 @@
 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
+xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
+xx=zy→x=y {x} {y} eq with trio< (od→ord x) (od→ord y) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
+
 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
-    lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
-    lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
-    lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
-    lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
-    lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
-    lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
-    lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
-    lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
-    lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
     lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
-    lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
+    lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
         lemma3 : ( x , x ) =h= ( y , z )
         lemma3 = ==-trans eq exg-pair
     lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
@@ -138,17 +139,24 @@
 ω-pair : {x y : HOD} → infinite ∋ x → infinite ∋ y → od→ord < x , y > o< next o∅
 ω-pair {x} {y} lx ly = lemma where
     lemma1 : od→ord x o< od→ord y → od→ord ( x , x ) o< od→ord ( x , y ) 
-    lemma1 = {!!}
-    lemma0 : od→ord x o< od→ord y → od→ord < x , y > o< osuc (next (od→ord (x , y)))
-    lemma0 x<y = begin
-         od→ord < x , y >
-       <⟨ ho< ⟩
+    lemma1 x<y with osuc-≡< (pair-xx<xy {x} {y})
+    lemma1 x<y | case1 eq = ⊥-elim ( o<¬≡ (cong (λ k → od→ord k ) (xx=zy→x=y (ord→== eq))) x<y ) 
+    lemma1 x<y | case2 lt = lt
+    lemma0 : od→ord x o< od→ord y → od→ord < x , y > o< next o∅
+    lemma0 x<y = osucprev (begin
+         osuc (od→ord < x , y >)
+       <⟨ osuc<nx ho< ⟩
          next (omax (od→ord (x , x)) (od→ord (x , y)))
        ≡⟨ cong (λ k → next k ) (sym (omax< _ _ (lemma1 x<y))) ⟩
          next (osuc (od→ord (x , y)))
        ≡⟨ sym (nexto≡) ⟩
          next (od→ord (x , y))
-       ∎ where open o≤-Reasoning O
+       ≤⟨ osucprev (ordtrans (next< ( omax<nx (<odmax infinite lx) (<odmax infinite ly))  (osuc<nx lemma2 )) (ordtrans <-osuc <-osuc )) ⟩
+         next o∅
+       ∎ ) where
+          open o≤-Reasoning O
+          lemma2 : next (od→ord (x , y)) o< next (omax (od→ord x) (od→ord y))
+          lemma2 = {!!}
     lemma : od→ord < x , y > o< next o∅
     lemma  with trio< (od→ord x) (od→ord y)
     lemma | tri< a ¬b ¬c = {!!}
@@ -172,7 +180,5 @@
 
  
 ZFP  : (A B : HOD) → HOD
-ZFP  A B = 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
+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 3fba5f805e50 -r 6dcea4c7cba1 Ordinals.agda
--- a/Ordinals.agda	Wed Jul 29 00:25:07 2020 +0900
+++ b/Ordinals.agda	Wed Jul 29 12:42:05 2020 +0900
@@ -265,6 +265,38 @@
         omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
         omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
 
+        x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
+        x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)    
+        x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
+             ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+        x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
+        x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
+             ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+
+        ≤next : {x y : Ordinal} → x o< y → next x o≤ next y
+        ≤next {x} {y} x<y with trio< (next x) y
+        ≤next {x} {y} x<y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
+        ≤next {x} {y} x<y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
+        ≤next {x} {y} x<y | tri> ¬a ¬b c = o≤-refl (x<ny→≡next x<y c)
+
+        x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
+        x<ny→≤next {x} {y} x<ny with trio< x y
+        x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next a
+        x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
+        x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
+
+        omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
+        omax<nomax {x} {y} with trio< x y
+        omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
+        omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+        omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+
+        omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
+        omax<nx {x} {y} {z} x<nz y<nz with trio< x y
+        omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
+        omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
+        omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal
diff -r 3fba5f805e50 -r 6dcea4c7cba1 generic-filter.agda
--- a/generic-filter.agda	Wed Jul 29 00:25:07 2020 +0900
+++ b/generic-filter.agda	Wed Jul 29 12:42:05 2020 +0900
@@ -139,7 +139,7 @@
 
 ω→2f≡i0 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
 ω→2f≡i0 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
-ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) {!!} p
+ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
 
 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
 ω→2f-iso X lt = record {