--- a/OD.agda	Mon Oct 07 01:28:11 2019 +0900
+++ b/OD.agda	Mon Dec 30 23:45:59 2019 +0900
@@ -36,16 +36,17 @@
 id : {A : Set n} → A → A
 id x = x
 
-eq-refl :  {  x :  OD  } → x == x
-eq-refl  {x} = record { eq→ = id ; eq← = id }
+==-refl :  {  x :  OD  } → x == x
+==-refl  {x} = record { eq→ = id ; eq← = id }
 
 open  _==_ 
 
-eq-sym :  {  x y :  OD  } → x == y → y == x
-eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
+==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
+==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
 
-eq-trans :  {  x y z :  OD  } → x == y → y == z → x == z
-eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
+==-sym : { x y  : OD } →  x == y →  y == x 
+==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
+
 
 ⇔→== :  {  x y :  OD  } → ( {z : Ordinal } → def x z ⇔  def y z) → x == y 
 eq→ ( ⇔→==  {x} {y}  eq ) {z} m = proj1 eq m 
@@ -74,7 +75,7 @@
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
   --   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x 
   --   ord→od x ≡ Ord x results the same
-  -- supermum as Replacement Axiom
+  -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound )
   sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
   sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ 
   -- contra-position of mimimulity of supermum required in Power Set Axiom
@@ -140,10 +141,10 @@
 ord→== : { x y : OD  } → od→ord x ≡  od→ord y →  x == y
 ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
    lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
-   lemma ox ox  refl = eq-refl
+   lemma ox ox  refl = ==-refl
 
 o≡→== : { x y : Ordinal  } → x ≡  y →  ord→od x == ord→od y
-o≡→==  {x} {.x} refl = eq-refl
+o≡→==  {x} {.x} refl = ==-refl
 
 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
@@ -162,7 +163,7 @@
 eq← ∅0 {w} lt = lift (¬x<0 lt)
 
 ∅< : { x y : OD  } → def x (od→ord y ) → ¬ (  x  == od∅  )
-∅<  {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
+∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
        
 ∅6 : { x : OD  }  → ¬ ( x ∋ x )    --  no Russel paradox
@@ -191,12 +192,6 @@
     right (case1 t) = case2 t
     right (case2 t) = case1 t
 
-==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
-==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
-
-==-sym : { x y  : OD } →  x == y →  y == x 
-==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
-
 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
 
@@ -339,15 +334,21 @@
 Def :  (A :  OD ) → OD 
 Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
 
-_⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
-_⊆_ A B {x} = A ∋ x →  B ∋ x
+-- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
+-- _⊆_ A B {x} = A ∋ x →  B ∋ x
+
+record _⊆_ ( A B : OD   ) : Set (suc n) where
+  field 
+     incl : { x : OD } → A ∋ x →  B ∋ x
+
+open _⊆_
 
 infixr  220 _⊆_
 
-subset-lemma : {A x y : OD  } → (  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( _⊆_ x A {y} )
-subset-lemma  {A} {x} {y} = record {
-      proj1 = λ z lt → proj1 (z  lt)
-    ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
+subset-lemma : {A x : OD  } → ( {y : OD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma  {A} {x} = record {
+      proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
+    ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
    } 
 
 open import Data.Unit
@@ -406,7 +407,7 @@
     -- infixr  230 _∩_ _∪_
     isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
-           isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
+           isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
        ;   pair→  = pair→
        ;   pair←  = pair←
        ;   union→ = union→
@@ -436,14 +437,14 @@
          empty : (x : OD  ) → ¬  (od∅ ∋ x)
          empty x = ¬x<0 
 
-         o<→c< :  {x y : Ordinal } {z : OD }→ x o< y → _⊆_  (Ord x) (Ord y) {z}
-         o<→c< lt lt1 = ordtrans lt1 lt
+         o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) 
+         o<→c< lt = record { incl = λ z → ordtrans z lt }  
          
-         ⊆→o< :  {x y : Ordinal } → (∀ (z : OD) → _⊆_  (Ord x) (Ord y) {z} ) →  x o< osuc y
+         ⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
          ⊆→o< {x} {y}  lt with trio< x y 
          ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
          ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
+         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
          ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
 
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
@@ -551,15 +552,15 @@
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 
-         ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x}
-         ord⊆power a x lt = power← (Ord a) x lemma where
-                lemma : {y : OD} → x ∋ y → Ord a ∋ y
-                lemma y<x with osuc-≡< lt
-                lemma y<x | case1 refl = c<→o< y<x
-                lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
+         ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
+         ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
+                lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+                lemma lt y<x with osuc-≡< lt
+                lemma lt y<x | case1 refl = c<→o< y<x
+                lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
 
-         -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
-         -- continuum-hyphotheis a x = ?
+         -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
+         -- continuum-hyphotheis a = ?
 
          --  assuming axiom of choice
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
@@ -620,12 +621,12 @@
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
                  lemma-ord  ox = TransFinite {ψ} induction ox where
                     ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
-                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
+                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
                     ∋-p A x | case1 (lift t)  = yes t
                     ∋-p A x | case2 t  = no (λ x → t (lift x ))
                     ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
                         → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
-                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x))
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
                     ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
                     ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
                          lemma : ¬ ((x : Ordinal ) → A x) →  B
@@ -643,8 +644,7 @@
                          lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
                          lemma = ∀-imply-or lemma1
                  have_to_find : choiced X
-                 have_to_find with lemma-ord (od→ord X )
-                 have_to_find | t = dont-or  t ¬¬X∋x where
+                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
                      ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
                      ¬¬X∋x nn = not record {
                             eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)