--- a/zf-in-agda.ind	Fri Jul 17 18:57:40 2020 +0900
+++ b/zf-in-agda.ind	Sat Jul 18 10:36:32 2020 +0900
@@ -811,6 +811,17 @@
    odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (def A (od y) → def (od B) y)  → def (od A) x → def (od B) x
    odef-iso refl t = t
 
+--The uniqueness of HOD
+
+To prove extensionality or other we need ==→o≡.
+
+Since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
+We can calculate the minimum using sup if we have bound but it is tedius.
+Only Select has non minimum odmax. 
+We have the same problem on 'def' itself, but we leave it, that is we assume the
+assumption of predicates of Agda have a unique form, it is something like the
+functional extensionality assumption.
+
 --Validity of Axiom of Extensionality
 
 If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, 
@@ -915,7 +926,6 @@
   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 ψ 
 
-
 --Axiom which have negation form
 
    Union, Selection