--- a/HOD.agda	Tue Jun 25 22:47:17 2019 +0900
+++ b/HOD.agda	Wed Jun 26 08:05:58 2019 +0900
@@ -48,8 +48,6 @@
    lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
    lemma {x}  x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
 
--- od∅ : {n : Level} → HOD {n} 
--- od∅ {n} = record { def = λ _ → Lift n ⊥ }
 od∅ : {n : Level} → HOD {n} 
 od∅ {n} = Ord o∅ 
 
@@ -60,7 +58,7 @@
   oiso   : {n : Level} {x : HOD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
-  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   -- necessary?
+  ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
   -- supermum as Replacement Axiom
@@ -246,9 +244,9 @@
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = sup-od ψ
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → y o< od→ord X  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
-       lemma :  {x : Ordinal} → ((y : Ordinal) → y o< od→ord X → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
-            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → y₁ o< od→ord X → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
+    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
+       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
+            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
        lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
            y<X : X ∋ ord→od y
            y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
@@ -289,7 +287,7 @@
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
-       ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
+       ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement = replacement
      } where
          open _∧_ 
@@ -349,10 +347,11 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (( X ∋ y ) ∧ ψ y ) ⇔ (Select X ψ ∋ y)
+         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
          selection {X} {ψ} {y} =  record { proj1 = λ s → record {
-            proj1 = λ y → {!!}  ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord (ord→od (od→ord y))} (proj1 s) refl (sym diso) } ;
-            proj2 = {!!} }
+             proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
+           ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
+                                  ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
          replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)