--- a/OD.agda	Fri Jul 03 22:22:59 2020 +0900
+++ b/OD.agda	Fri Jul 03 22:54:45 2020 +0900
@@ -53,17 +53,25 @@
 eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m 
 
 -- next assumptions are our axiom
+--
+--  OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one
+--  correspondence to the OD then the OD looks like a ZF Set.
+--
+--  If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e.
+--  bbounded ODs are ZF Set. Unbounded ODs are classes.
+--
 --  In classical Set Theory, HOD is used, as a subset of OD, 
 --     HOD = { x | TC x ⊆ OD }
 --  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
---  This is not possible because we don't have V yet.
+--  This is not possible because we don't have V yet. So we assumes HODs are bounded OD.
 --
 --  We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
---  ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD.
+--  There two contraints on the HOD order, one is ∋, the other one is ⊂.
+--  ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary
+--  bound on each HOD.
 --
---  In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
+--  In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
 --  we need explict assumption on sup.
---  In order to allow sup on od→ord HOD, solutions of a HOD have to have a maximu.
 --
 --  ==→o≡ is necessary to prove axiom of extensionality.
 
@@ -90,8 +98,8 @@
   c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
   ⊆→o≤  :   {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
   oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  ==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
+  diso   :  {x : Ordinal }  → od→ord ( ord→od x ) ≡ x
+  ==→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 ψ 
 
@@ -313,7 +321,7 @@
         lemma {o∅} iφ = proj1 next-limit
         lemma (isuc {x} i) = lemma1 where -- proj2 next-limit ? ( lemma i )
            lemma1 : od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅
-           lemma1 = ?
+           lemma1 = {!!}