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

diff -r 6dcea4c7cba1 -r 6eaab908130e OPair.agda
--- a/OPair.agda	Wed Jul 29 12:42:05 2020 +0900
+++ b/OPair.agda	Wed Jul 29 21:51:00 2020 +0900
@@ -137,37 +137,28 @@
 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 = lemma where
-    lemma1 : od→ord x o< od→ord y → od→ord ( x , x ) o< od→ord ( x , y ) 
-    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
+ω-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∅
+    lemma0 = 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))) ⟩
+       ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
          next (osuc (od→ord (x , y)))
        ≡⟨ sym (nexto≡) ⟩
          next (od→ord (x , y))
-       ≤⟨ osucprev (ordtrans (next< ( omax<nx (<odmax infinite lx) (<odmax infinite ly))  (osuc<nx lemma2 )) (ordtrans <-osuc <-osuc )) ⟩
+       ≤⟨ x<ny→≤next lemma3 ⟩
          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 = {!!}
-    lemma | tri≈ ¬a b ¬c = next< {!!} {!!}
-    lemma | tri> ¬a ¬b c = {!!}
 
 _⊗_ : (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 = {!!}
+-- 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 = {!!} }
 
 record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p )  : Set (suc n) where
   field
@@ -175,10 +166,10 @@
     π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 = {!!} }
+-- 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 (odmax A) (odmax B) ; <odmax = λ {y} px → {!!}  } -- (<odmax A (proj2 px (proj1 px) ))
+-- 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 6dcea4c7cba1 -r 6eaab908130e Ordinals.agda
--- a/Ordinals.agda	Wed Jul 29 12:42:05 2020 +0900
+++ b/Ordinals.agda	Wed Jul 29 21:51:00 2020 +0900
@@ -172,6 +172,14 @@
         omax<  x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
         omax<  x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
 
+        omax≤ :  ( x y : Ordinal  ) → x o≤ y → osuc y ≡ omax x y
+        omax≤  x y le with trio< x y
+        omax≤  x y le | tri< a ¬b ¬c = refl
+        omax≤  x y le | tri≈ ¬a refl ¬c = refl
+        omax≤  x y le | tri> ¬a ¬b c with osuc-≡< le
+        omax≤ x y le | tri> ¬a ¬b c | case1 eq = ⊥-elim (¬b eq)
+        omax≤ x y le | tri> ¬a ¬b c | case2 x<y = ⊥-elim (¬a x<y)
+
         omax≡ :  ( x y : Ordinal  ) → x ≡ y → osuc y ≡ omax x y
         omax≡  x y eq with trio< x y
         omax≡  x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
@@ -273,15 +281,17 @@
         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)
+        ≤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 with osuc-≡< x≤y
+        ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl refl   -- x = y < next x
+        ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl (x<ny→≡next x<y c) -- x ≤ y < next x 
 
         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 ¬b ¬c =  ≤next (ordtrans a <-osuc )
         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 ))
 
diff -r 6dcea4c7cba1 -r 6eaab908130e generic-filter.agda
--- a/generic-filter.agda	Wed Jul 29 12:42:05 2020 +0900
+++ b/generic-filter.agda	Wed Jul 29 21:51:00 2020 +0900
@@ -137,15 +137,19 @@
 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
 ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
 
-ω→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 ) (nat→ω-iso iω) p
+ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
+ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
+
+open _⊆_
 
 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
 ω→2f-iso X lt = record {
      eq→ = eq1
    ; eq← = eq2
   } where
+     X⊆ω : {x : HOD } → X ∋ x → infinite ∋ x
+     X⊆ω {x} x<X = incl (ODC.power→⊆ O infinite X lt ) x<X
      eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x
      eq1 {x} fx = {!!} where
          x-nat : odef infinite x
@@ -158,7 +162,7 @@
      eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x
      eq2 {x} Xx = {!!} where
          x-nat : odef infinite x
-         x-nat = {!!}
+         x-nat = subst ( λ k → odef infinite k ) diso ( X⊆ω (subst(λ k → odef X  k ) (sym diso ) Xx) )
   
 fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
 fω→2-iso f = f-extensionality (λ x → eq1 x ) where