# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558777535 -32400
# Node ID 264784731a67c6781c7aa95f24feabe5c38629ea
# Parent  e584686a1307277abccef56d440b2c7c634d362a
clean up

diff -r e584686a1307 -r 264784731a67 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat May 25 09:09:40 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 18:45:35 2019 +0900
@@ -36,9 +36,6 @@
 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
 x c< a = a ∋ x 
 
--- _=='_  :  {n : Level} → Set (suc n) -- Rel (OD {n}) (suc n)
--- _=='_  {n} =  ( a b :  OD {n} ) → (  ∀ { x : OD {n} } → a ∋ x → b ∋ x ) ∧  ( ∀ { x : OD {n} } → a ∋ x → b ∋ x ) 
-
 record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
   field
      eq→ : ∀ { x : Ordinal {n} } → def a x → def b x 
@@ -64,8 +61,6 @@
 od∅ : {n : Level} → OD {n} 
 od∅ {n} = record { def = λ _ → Lift n ⊥ }
 
-open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
-
 postulate      
   c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
   o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
@@ -74,15 +69,10 @@
   sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
   sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → ψ x  c< sup-od ψ
   ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
-  ∅-base-lv : {n : Level} → lv ( od→ord (od∅ {n}) ) ≡ lv (o∅ {n})
-  ∅-base-d : {n : Level} → ord ( od→ord (od∅ {n}) ) ≅ ord (o∅ {n})
 
 o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
 o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
 
-od∅→o∅ : {n : Level} →  od→ord (od∅ {n} ) ≡ o∅ {n} 
-od∅→o∅  = ordinal-cong ∅-base-lv ∅-base-d
-
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
 
@@ -110,9 +100,6 @@
    ... | t with t (case2 (s< ℵΦ<   )) 
    c3 .(Suc lx) (ℵ lx) d not | t | ()
 
--- find : {n : Level} → ( x : Ordinal {n} ) → o∅ o< x → Ordinal {n}  
--- exists : {n : Level} → ( x : Ordinal {n} ) → (0<x : o∅ o< x ) → find x 0<x o< x
-
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
@@ -141,47 +128,18 @@
 ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lx ; ord = Φ (Suc lx) } ; min<x = case2 ℵΦ<  }
 ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case2 ())
 
-∅4 : {n : Level} →  ( x : OD {n} )  →  x  ≡ od∅ {n}  → od→ord x ≡ o∅ {n}
-∅4 {n} x refl =  ∅3 lemma1 where
-  lemma0 :  (y : Ordinal {n}) → def ( od∅ {n} ) y →  ⊥
-  lemma0 y (lift ())
-  lemma1 : (y : Ordinal {n}) → y o< od→ord od∅ → ⊥
-  lemma1 y y<o = lemma0 y ( def-subst {n} {ord→od (od→ord od∅ )} {od→ord (ord→od y)} (o<→c< y<o) oiso diso )
-
 ∅5 : {n : Level} →  ( x : Ordinal {n} )  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} record { lv = Zero ; ord = (Φ .0) } not = ⊥-elim (not refl) 
 ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
 ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
 
-postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
-
-∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅
-∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x
-∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl
-∅6 {n} x lt refl | tri≈ ¬a b ¬c =  ¬a lt
-∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl
-
 ∅8 : {n : Level} →  ( x : Ordinal {n} )  → ¬  x o< o∅ {n}
 ∅8 {n} x (case1 ())
 ∅8 {n} x (case2 ())
 
--- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y))   →  x ≡ od∅ 
--- ∅10 {n} x not = ?
-
--- ∅77 : {n : Level} → (x : OD {suc n} ) →  ¬ ( ord→od (o∅ {suc n}) ∋ x )
--- ∅77 {n} x lt = {!!} where
-
-∅7' : {n : Level} → ord→od (o∅ {n}) == od∅ {n} 
-∅7' {n} = record { eq→ = e1 ;  eq← = e2 } where
-   e2 : {y : Ordinal {n}} → def od∅ y → def (ord→od (o∅ {n})) y 
-   e2 {y} (lift ())
-   e1 : {x : Ordinal {n} } → def (ord→od (o∅ {n})) x → def (od∅ {n})  x
-   e1 {x} o<x = def-subst {n} {ord→od (o∅ {n})} {x} o<x (cong (λ k → record { def = k }) ∅-base-def ) refl
-
 ord-iso : {n : Level} {y : Ordinal {n} } → record { lv = lv (od→ord (ord→od y)) ; ord = ord (od→ord (ord→od y)) } ≡ record { lv = lv y ; ord = ord y }
 ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
 
-
 ∅7 : {n : Level} →  ( x : OD {n} ) → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
 ∅7 {n} x eq = record { eq→ = e1 eq ; eq← = e2 } where
    e2 : {y : Ordinal {n}} → def od∅ y → def x y 
@@ -191,7 +149,6 @@
    e1 {o∅} {y} refl x>y | Zero   = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
    e1 {o∅} {y} refl x>y | Suc lx = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
 
-
 open _∧_
 
 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
@@ -199,7 +156,6 @@
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7 x eq )
 
-
 OD→ZF : {n : Level} → ZF {suc n} {n}
 OD→ZF {n}  = record { 
     ZFSet = OD {n}
@@ -217,9 +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 → select ( ord→od x ) } where
-       select : OD {n} → Set n
-       select x = ψ x
+    Select X ψ = record { def = λ 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}
@@ -276,12 +230,11 @@
             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 x (λ x₁ → (( minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)))
          proj1 ( regularity x non ) =  minimul<x x non 
-         proj2 ( regularity x non ) = {!!} where -- cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) )   where
-            not-min : ( z : Ordinal {n} ) →  ¬ ( def (Select x (λ y → (minimul x non ∋ y) ∧  (x ∋ y))) z  )
-            not-min z = {!!}
-            lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y →  (minimul x non ∋ y) ∧  (x ∋ y))) z ≡ Lift n ⊥ 
-            lemma0 z = {!!}
+         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 = {!!}
+            reg1 :  Select (minimul x non , x) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
+            reg1 = record { eq→ = {!!} ; eq← = λ () }