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

diff -r 619e68271cf8 -r d9f3774ddb00 src/OD.agda
--- a/src/OD.agda	Mon May 22 19:06:25 2023 +0900
+++ b/src/OD.agda	Sat May 27 18:41:04 2023 +0900
@@ -91,21 +91,33 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
+_,_ : HOD  → HOD  → HOD
+
 record ODAxiom : Set (suc n) where
- field
-  -- HOD is isomorphic to Ordinal (by means of Goedel number)
-  & : HOD  → Ordinal
-  * : Ordinal  → HOD
-  c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
-  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
-  *iso   :  {x : HOD }      → * ( & x ) ≡ x
-  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
-  ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
-  ∋-irr : {X : HOD} {x : Ordinal } → (a b : def (od X) x) → a ≅ b
+   field
+      -- HOD is isomorphic to Ordinal (by means of Goedel number)
+      & : HOD  → Ordinal
+      * : Ordinal  → HOD
+      ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
+      c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y   -- inferred from pair-omax
+      *iso   :  {x : HOD }      → * ( & x ) ≡ x
+      &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
+      ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
+      ∋-irr : {X : HOD} {x : Ordinal } → (a b : def (od X) x) → a ≅ b
+      pair-omax : {x y : HOD} → & (x , y) ≡ omax (& x) (& y) 
 
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
+-- the pair
+x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ; <odmax = lemma }  where
+        lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
+        lemma {t} (case1 refl) = omax-x  _ _
+        lemma {t} (case2 refl) = omax-y  _ _
+
+x,x=ox : {x : HOD } → & (x , x) ≡ osuc (& x)
+x,x=ox {x} = trans pair-omax (sym ( omax≡ _ _ refl ))
+
 -- possible order restriction (required in the axiom of infinite )
 
 record ODAxiom-ho< : Set (suc n) where
@@ -254,37 +266,16 @@
 odef∧< : {A : HOD } {y : Ordinal} {n : Level } → {P : Set n} → odef A y ∧ P → y o< & A
 odef∧< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
 
--- the pair
-_,_ : HOD  → HOD  → HOD
-x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ; <odmax = lemma }  where
-    lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
-    lemma {t} (case1 refl) = omax-x  _ _
-    lemma {t} (case2 refl) = omax-y  _ _
+-- another possible restriction. We require no minimality on odmax, so it may arbitrary larger.
+odmax<&  : { x y : HOD } → x ∋ y →  Set n
+odmax<& {x} {y} x∋y = odmax x o< & x
 
--- {x y : HOD} → & (x , y) ≡ omax (& x) (& y) 
-
-pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
+pair<y : {x y : HOD } → def (od 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
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
--- another possible restriction. We require no minimality on odmax, so it may arbitrary larger.
-odmax<&  : { x y : HOD } → x ∋ y →  Set n
-odmax<& {x} {y} x∋y = odmax x o< & x
-
-in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ & (ψ (* y )))))  }
-
-_∩_ : ( A B : HOD ) → HOD
-A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
-        ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
-
-_⊆_ : ( A B : HOD)   → Set n
-_⊆_ A B = { x : Ordinal } → odef A x → odef B x
-
-infixr  220 _⊆_
-
 -- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
 ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
    →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
@@ -302,6 +293,19 @@
     lemma1 : osuc (& y) o< & (x , x)
     lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c )
 
+
+in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ & (ψ (* y )))))  }
+
+_∩_ : ( A B : HOD ) → HOD
+A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
+        ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
+
+_⊆_ : ( A B : HOD)   → Set n
+_⊆_ A B = { x : Ordinal } → odef A x → odef B x
+
+infixr  220 _⊆_
+
 ε-induction : { ψ : HOD  → Set (suc n)}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
@@ -444,6 +448,9 @@
 Intersection : (X : HOD ) → HOD   -- ∩ X
 Intersection X = record { od = record { def = λ x → (x o≤ & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = osuc (& X) ; <odmax = λ lt → proj1 lt } 
 
+empty : (x : HOD  ) → ¬  (od∅ ∋ x)
+empty x = ¬x<0
+
 
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
@@ -465,37 +472,31 @@
 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 = 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
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = osuc (& (Ord (next o∅))) ; <odmax = lemma }  
+   where
+      u : (y : Ordinal ) → HOD
+      u y = Union (* y , (* y , * y))
+      --- main recursion
+      lemma : {y : Ordinal} → infinite-d y → y o< osuc (& (Ord (next o∅)))
+      lemma {o∅} iφ = b<x→0<x <-osuc 
+      lemma (isuc {y} iy) = ⊆→o≤ lemma2 where
+          lemma0 : y o< osuc (& (Ord (next o∅)))
+          lemma0 = lemma iy
+          lemma2 :  {z : Ordinal} → Own (* y , (* y , * y)) z → z o< next o∅
+          lemma2 {z} record { owner = yo ; ao = (case1 eq) ; ox = oyz } = ?
+          lemma2 {z} record { owner = yo ; ao = (case2 eq) ; ox = oyz } = ?
+      lemma-i : {y : Ordinal} → infinite-d y → * y ⊆ Ord (next o∅)
+      lemma-i {.(Ordinals.o∅ O)} iφ {x} x<0 = ⊥-elim ( empty (* x) (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) x<0) )
+      lemma-i {.(& (Union (* z , (* z , * z))))} (isuc {z} iz) {x} ux = lemma3 where
+          lemma4 : * z ⊆ Ord (next o∅)
+          lemma4 = lemma-i iz
+          lemma3 : x o< next o∅
+          lemma3 with subst (λ k → odef k x) *iso ux
+          ... | record { owner = oz ; ao = case1 eq ; ox = ozx } = lemma-i iz (subst (λ k → odef k x) (trans (cong (*) eq) *iso )  ozx)
+          ... | record { owner = oz ; ao = case2 eq ; ox = ozx } with subst (λ k → odef k x) (trans (cong (*) eq) *iso ) ozx
+          ... | case1 eq1 = lemma-i iz ?
+          ... | case2 eq1 = ?
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))