--- a/OD.agda	Tue Jul 07 15:32:11 2020 +0900
+++ b/OD.agda	Sun Jul 12 12:32:42 2020 +0900
@@ -103,6 +103,9 @@
   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 ψ 
 
+--  another form of infinite
+--  pair-ord< :  {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x)
+
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
@@ -212,7 +215,7 @@
 is-o∅ x | tri> ¬a ¬b c = no ¬b
 
 -- the pair
-_,_ : HOD  → HOD  → HOD 
+_,_ : HOD  → HOD  → HOD  
 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x)  (od→ord y) ; <odmax = lemma }  where
     lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
     lemma {t} (case1 refl) = omax-x  _ _
@@ -247,13 +250,21 @@
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
--- ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
---    →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
---    →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y 
--- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y)
--- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
--- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → def (od k)  (od→ord x)) {!!} y∋x)))
--- ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → def (od k)  (od→ord x)) {!!} y∋x)))
+⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
+   →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
+   →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y 
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y)
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x )))
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c =
+  ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where
+    lemma : {z : Ordinal} → (z ≡ od→ord x) ∨ (z ≡ od→ord x) → od→ord x ≡ z
+    lemma (case1 refl) = refl
+    lemma (case2 refl) = refl
+    y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
+    y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
+    lemma1 : osuc (od→ord y) o< od→ord (x , x)
+    lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) 
 
 subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
@@ -347,10 +358,10 @@
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
     -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
-    -- We simply assumes nfinite-d y has a maximum.
+    -- We simply assumes infinite-d y has a maximum.
     -- 
-    -- This means that many of OD cannot be HODs because of the od→ord mapping divergence.
-    -- We should have some axioms to prevent this, but it may complicate thins.
+    -- 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.
     -- 
     postulate
         ωmax : Ordinal
@@ -359,6 +370,17 @@
     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 = next o∅ ; <odmax = lemma }  where
+    --     u : (y : Ordinal ) → HOD
+    --     u y = Union (ord→od y , (ord→od y , ord→od y))
+    --     lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+    --     lemma {o∅} iφ = {!!}
+    --     lemma (isuc {y} x) = {!!} where
+    --         lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y )))
+    --         lemma1 = {!!}
+        
+
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y