--- a/ordinal-definable.agda	Mon May 27 15:36:03 2019 +0900
+++ b/ordinal-definable.agda	Mon May 27 16:14:35 2019 +0900
@@ -228,6 +228,12 @@
 is-od∅ {n} x | tri< (case2 ()) ¬b ¬c
 is-od∅ {n} x | tri> ¬a ¬b c = no ( ∅2 c )
 
+is-∋ : {n : Level} →  ( x y : OD {suc n} ) → Dec ( x ∋ y )
+is-∋ {n} x y with tri-c< x y
+is-∋ {n} x y | tri< a ¬b ¬c = no ¬c
+is-∋ {n} x y | tri≈ ¬a b ¬c = no ¬c
+is-∋ {n} x y | tri> ¬a ¬b c = yes c
+
 open _∧_
 
 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
@@ -285,7 +291,7 @@
        ;   regularity = regularity
        ;   infinity∅ = {!!}
        ;   infinity = {!!}
-       ;   selection = {!!}
+       ;   selection = selection
        ;   replacement = {!!}
      } where
          open _∧_ 
@@ -299,6 +305,8 @@
          union→ X x y X∋x x∋y = {!!}  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
+         selection : {ψ : OD → Set n} (X y : OD) → Select X ψ ∋ y → ψ y
+         selection = {!!}
          minord : (x : OD {n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
          minord x not = ominimal (od→ord x) (∅9 x not)
          minimul : (x : OD {n} ) → ¬ (x == od∅ )→ OD {n} 
@@ -311,15 +319,12 @@
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 ( regularity x non ) =  minimul<x x non 
          proj2 ( regularity x non ) = reg1 where
-            reg4 : {y : Ordinal} → (y ≡ od→ord (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq))))))) ∨ (y ≡ od→ord x)
-            reg4 {y} = {!!}
             reg2 : {y : Ordinal} → ( def (minimul x non) y )
                → ( def (minimul x non) y → (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 
-            reg2 {y} or t with t or
-            reg2 s t | record { proj1 = proj1 ; proj2 = proj2 } = {!!}
-            reg0 : {y : Ordinal} → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
-            reg0 {y} t with (reg2 {y}) {!!} t
-            reg0 {y} t | ()
+            reg2 = {!!}
+            reg0 : {y : Ordinal {n}} → Minimumo (od→ord x) → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
+            reg0 {y} m t with {!!} y (mino (minord x non))
+            ... | lt = {!!}
             reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
-            reg1 = record { eq→ =  reg0 ; eq← = λ () }
+            reg1 = record { eq→ =  reg0 (minord x non) ; eq← = λ () }