# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1684749985 -32400
# Node ID 619e68271cf82b86e5e30e930528d91f0ce61698
# Parent  302cfb533201cb79a60777849bbb58e71db5a59c
...

diff -r 302cfb533201 -r 619e68271cf8 src/OD.agda
--- a/src/OD.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/OD.agda	Mon May 22 19:06:25 2023 +0900
@@ -261,6 +261,8 @@
     lemma {t} (case1 refl) = omax-x  _ _
     lemma {t} (case2 refl) = omax-y  _ _
 
+-- {x y : HOD} → & (x , y) ≡ omax (& x) (& y) 
+
 pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
    lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
@@ -460,28 +462,37 @@
 --
 --  Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
 
+infinite-od : OD
+infinite-od = record { def = λ x → infinite-d x } 
+
+postulate 
+    infinite-odmax : Ordinal 
+    infinite-odmax< : {z : Ordinal } → def infinite-od z → z o< infinite-odmax
+
 infinite : HOD
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    u : (y : Ordinal ) → HOD
-    u y = Union (* y , (* y , * y))
-    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
-    lemma8 = ho<
-    ---           (x,y) < next (omax x y) < next (osuc y) = next y
-    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
-    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
-    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
-    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
-    lemma9 = lemmaa (c<→o< (case1 refl))
-    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
-    lemma71 = next< lemma81 lemma9
-    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
-    lemma1 = ho<
-    --- main recursion
-    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    lemma {o∅} iφ = x<nx
-    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = infinite-odmax ; <odmax = infinite-odmax< }  
+
+-- where
+--    u : (y : Ordinal ) → HOD
+--    u y = Union (* y , (* y , * y))
+--    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+--    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
+--    lemma8 = ho<
+--    ---           (x,y) < next (omax x y) < next (osuc y) = next y
+--    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
+--    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
+--    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
+--    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+--    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
+--    lemma9 = lemmaa (c<→o< (case1 refl))
+--    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
+--    lemma71 = ? -- next< lemma81 lemma9
+--    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
+--    lemma1 = ho<
+--    --- main recursion
+--    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+--    lemma {o∅} iφ = x<nx
+--    lemma (isuc {y} x) = ? -- next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
 
 empty : (x : HOD  ) → ¬  (od∅ ∋ x)
 empty x = ¬x<0
diff -r 302cfb533201 -r 619e68271cf8 src/ODUtil.agda
--- a/src/ODUtil.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/ODUtil.agda	Mon May 22 19:06:25 2023 +0900
@@ -75,11 +75,15 @@
    lemma {z} (case1 refl) = case1 refl
    lemma {z} (case2 refl) = case1 refl
 
-pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
-... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
-... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
+-- pair-<xy : {x y : HOD} → {z : Ordinal}  → & x o< next z →  & y o< next z  → & (x , y) o< next z
+-- pair-<xy {x} {y} {z} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
+-- ... | tri< a ¬b ¬c | record { eq = eq1 } = ? where
+--     ll1 : omax (& x) (& y) o< next z
+--     ll1 = subst (λ k → k o< next z ) (sym eq1) (osuc<nx y<nn) 
+--     ll2 : & (x , y) o< next (omax (& x) (& y)) 
+--     ll2 = ho<
+-- ... | tri> ¬a ¬b c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
+-- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ? -- next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
 
 --  another form of infinite
 -- pair-ord< :  {x : Ordinal } → Set n
@@ -115,7 +119,7 @@
     ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
    }
 
-ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< infinite-odmax
 ω<next-o∅ {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD
diff -r 302cfb533201 -r 619e68271cf8 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/OrdUtil.agda	Mon May 22 19:06:25 2023 +0900
@@ -259,29 +259,11 @@
 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
-next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-next< {x} {y} {z} x<nz y<nx with trio< y (next z)
-next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
-next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
-   (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
-next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
-   (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
-
 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
 osuc< {x} {y} refl = <-osuc
 
 nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
-nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
-
-nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
-nexto≡ {x} with trio< (next x) (next (osuc x) )
---    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
-nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
-   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
-nexto≡ {x} | tri≈ ¬a b ¬c = b
---    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
-nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
-   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+nexto=n {x} {y} lt = subst (λ k → x o< k ) (sym nexto≡) lt
 
 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
@@ -291,33 +273,33 @@
 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 ))))
+-- 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 with osuc-≡< x≤y
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
+-- ≤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 -- x = y < next x
+-- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (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 (ordtrans a <-osuc )
-x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
-x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
+-- 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 (ordtrans a <-osuc )
+-- x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
+-- x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (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<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
@@ -325,11 +307,11 @@
 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
 
-nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
-nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
-nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
-nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
-nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
+-- nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
+-- nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
+-- nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
+-- nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
+-- nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
 
 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
   field
diff -r 302cfb533201 -r 619e68271cf8 src/Ordinals.agda
--- a/src/Ordinals.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/Ordinals.agda	Mon May 22 19:06:25 2023 +0900
@@ -33,8 +33,8 @@
 record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
      x<nx :    { y : ord } → (y o< next y )
+     nexto≡ : {x : ord} → next x ≡ next (osuc x)
      osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 
-     ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
diff -r 302cfb533201 -r 619e68271cf8 src/ZProduct.agda
--- a/src/ZProduct.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/ZProduct.agda	Mon May 22 19:06:25 2023 +0900
@@ -35,7 +35,7 @@
 open _==_
 
 <_,_> : (x y : HOD) → HOD
-< x , y > = (x , x ) , (x , y )
+< x , y > = (x , x) , (x , y)
 
 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
@@ -113,6 +113,11 @@
 --     lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >)
 --     lemma2 = ? -- replacement← A a A∋a ?
 
+--  & (x , x) o< next (osuc (& x))
+--  & (x , y) o< next (omax (& x) (& y))
+--  & ((x , x) , (x , y)) o< next (omax (next (osuc (& x))) (next (omax (& x) (& y))))
+--                        o≤ next (next (omax (& A) (& B)))
+
 data ZFProduct  (A B : HOD) : (p : Ordinal) → Set n where
     ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
 
@@ -121,10 +126,10 @@
         ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
    where
         lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
-        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b
-        ... | tri< a<b ¬b ¬c = ?
-        ... | tri≈ ¬a a=b ¬c = ?
-        ... | tri> ¬a ¬b b<a = ?
+        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b | inspect (omax a) b
+        ... | tri< a<b ¬b ¬c | record { eq = eq1 } = ?
+        ... | tri≈ ¬a a=b ¬c | record { eq = eq1 } = ?
+        ... | tri> ¬a ¬b b<a | record { eq = eq1 } = ?
 
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb )