--- a/HOD.agda	Tue Jun 25 21:05:07 2019 +0900
+++ b/HOD.agda	Tue Jun 25 22:47:17 2019 +0900
@@ -3,7 +3,6 @@
 
 open import zf
 open import ordinal
-
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties 
@@ -246,12 +245,13 @@
  } where
     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} ) → X ∋ x → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → (d : def X x)  → f x d ; otrans = λ {x} g {y} d1 → {!!} }  where
-       f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n) 
-       f x d = ψ (ord→od x)  (subst (λ k → def X k ) (sym diso) d)
-       ftrans' : {x : Ordinal} ( g : (x : Ordinal {suc n} ) (d : def X x ) → f x d ) → {y : Ordinal} → y o< x → (d : def X y) → f y d
-       ftrans' {x} g {y} y<x d = g y d
+    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)
+       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)  )
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}
@@ -265,7 +265,7 @@
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = Select (A , B) (  λ x d → ( A ∋ x ) ∧ (B ∋ x) )
+    A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     ｛_｝ : ZFSet → ZFSet
@@ -349,8 +349,10 @@
          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 ) →  x ∈ X  → Set (suc n)} {y : HOD} → ((d : X ∋ y ) → ψ y d ) ⇔ (Select X ψ ∋ y)
-         selection {ψ} {X} {y} =  {!!}
+         selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (( X ∋ y ) ∧ ψ 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 = {!!} }
          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∅) 
@@ -358,10 +360,10 @@
          minimul : (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n} 
          minimul x  not = {!!}
          regularity :  (x : HOD) (not : ¬ (x == od∅)) →
-            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ d → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = {!!}
          proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where
-            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ d → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
+            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
             reg {y} t = {!!}
          extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d