# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595086015 -32400
# Node ID f74681db63c7834129f9240dc03073135d0d928d
# Parent  1a8ca713bc32b77e32a8836b977d111f541bbb58
...

diff -r 1a8ca713bc32 -r f74681db63c7 OD.agda
--- a/OD.agda	Sat Jul 18 18:11:13 2020 +0900
+++ b/OD.agda	Sun Jul 19 00:26:55 2020 +0900
@@ -103,6 +103,9 @@
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
   sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
+-- possible order restriction
+  ho< : {x : HOD} → od→ord x o< next (odmax x)
+
 
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
@@ -117,10 +120,6 @@
 odmaxmin : Set (suc n)
 odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z
 
--- possible order restriction
-hod-ord< :  {x : HOD } → Set n
-hod-ord< {x} =  od→ord x o< next (odmax x)
-
 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
 ¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
@@ -374,15 +373,15 @@
 -- This means that many of OD may not be HODs because of the od→ord mapping divergence.
 -- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
 -- 
-postulate
-    ωmax : Ordinal
-    <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+-- postulate
+--     ωmax : Ordinal
+--     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+-- 
+-- infinite : HOD 
+-- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
 
 infinite : HOD 
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
-
-infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
-infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
     u : (y : Ordinal ) → HOD
     u y = Union (ord→od y , (ord→od y , ord→od y))
     --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
@@ -405,7 +404,7 @@
     lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
 
 ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
-ω<next-o∅ ho< {y} lt = <odmax (infinite' ho<) lt
+ω<next-o∅ ho< {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD
 nat→ω Zero = od∅
@@ -418,8 +417,10 @@
     lemma (isuc lt) = Suc (lemma lt)
 
 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
-ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
-ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
+ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
+ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
+    lemma :  od→ord (Union (ord→od (od→ord (nat→ω n)) , (ord→od (od→ord (nat→ω n)) , ord→od (od→ord (nat→ω n))))) ≡ od→ord (nat→ω (Suc n))
+    lemma = subst (λ k → od→ord (Union (k , ( k , k ))) ≡ od→ord (nat→ω (Suc n))) (sym oiso) refl
 
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
diff -r 1a8ca713bc32 -r f74681db63c7 OPair.agda
--- a/OPair.agda	Sat Jul 18 18:11:13 2020 +0900
+++ b/OPair.agda	Sun Jul 19 00:26:55 2020 +0900
@@ -135,6 +135,25 @@
 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< osuc (next o∅)
+ω-pair {x} {y} lx ly with trio< (od→ord x) (od→ord y)
+ω-pair {x} {y} lx ly | tri≈ ¬a b ¬c = {!!}
+ω-pair {x} {y} lx ly | tri< a ¬b ¬c = {!!}
+ω-pair {x} {y} lx ly | tri> ¬a ¬b c = {!!}
+-- ω-pair {x} {y} lx ly = begin
+--       od→ord < x , y >
+--     <⟨ ho< ⟩
+--       next (omax (od→ord (x , x)) (od→ord (x , y)))
+--     ≤⟨ {!!} ⟩
+--       next (omax (od→ord (x , x)) (od→ord (x , y)))
+--     ≡⟨ cong (λ k → next k ) (sym (omax< _ _ {!!} )) ⟩
+--       next (osuc (od→ord (x , y)))
+--     ≤⟨ {!!} ⟩
+--       od→ord < ord→od (next o∅)  , ord→od (next o∅)  >
+--     ≤⟨ {!!} ⟩
+--       next o∅ 
+--     ∎ where open o≤-Reasoning O
+
 _⊗_ : (A B : HOD) → HOD
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
@@ -151,8 +170,8 @@
 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 ) } ;
+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
diff -r 1a8ca713bc32 -r f74681db63c7 filter.agda
--- a/filter.agda	Sat Jul 18 18:11:13 2020 +0900
+++ b/filter.agda	Sun Jul 19 00:26:55 2020 +0900
@@ -155,10 +155,6 @@
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
-postulate  
-   ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
-
-
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
   h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →