# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558784900 -32400
# Node ID 7c23969befc97c94be27c8ed2169deb6e10e3ca1
# Parent  4fb2a239061dec6527c346e16d956de91528d056
fix Select

diff -r 4fb2a239061d -r 7c23969befc9 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat May 25 18:45:47 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 20:48:20 2019 +0900
@@ -173,7 +173,7 @@
     Replace : OD {n} → (OD {n} → OD {n} ) → OD {n}
     Replace X ψ = sup-od ψ
     Select : OD {n} → (OD {n} → Set n ) → OD {n}
-    Select X ψ = record { def = λ x → ψ ( ord→od x ) } 
+    Select X ψ = record { def = λ x → ( ( def X  x ) ∧ ψ ( ord→od x )) } 
     _,_ : OD {n} → OD {n} → OD {n}
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {n} → OD {n}
@@ -228,13 +228,17 @@
          minimul<x x not = lemma0 (min<x (minord x not)) where
             lemma0 : mino (minord x not)  o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
             lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
-         regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧
-            (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+         regularity :  (x : OD) (not : ¬ (x == od∅)) →
+            (x ∋ minimul x not) ∧ (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 ( regularity x non ) =  minimul<x x non 
          proj2 ( regularity x non ) = reg1 where
-            reg0 : { x₁ : Ordinal} → def (Select (minimul x non , x) (λ x₂ → (minimul x non ∋ x₂) ∧ (x ∋ x₂))) x₁
-                    → def od∅ x₁
-            reg0 {x₁} t = {!!}
+            reg3 : {y : Ordinal} → ((y ≡ od→ord (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
+                ∧ ( def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 x eq)))))) (od→ord (ord→od y))
+                ∧ def x (od→ord (ord→od y))) → Lift n ⊥
+            reg3 = {!!}
+            reg0 : {y : Ordinal} → def (Select (minimul x non , x)
+                     (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
+            reg0 {y} t = reg3 t
             reg1 :  Select (minimul x non , x) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
-            reg1 = record { eq→ = {!!} ; eq← = λ () }
+            reg1 = record { eq→ =  reg0 ; eq← = λ () }