# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559010703 -32400
# Node ID 419688a279e0f1d4a84742f854492c887cadca31
# Parent  aad8cdce8845464df200dcfaef86c2dac5a2b522
...

diff -r aad8cdce8845 -r 419688a279e0 ordinal-definable.agda
--- a/ordinal-definable.agda	Tue May 28 00:07:23 2019 +0900
+++ b/ordinal-definable.agda	Tue May 28 11:31:43 2019 +0900
@@ -128,10 +128,10 @@
 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 ())
 
-∅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)
+∅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)
 
 ∅8 : {n : Level} →  ( x : Ordinal {n} )  → ¬  x o< o∅ {n}
 ∅8 {n} x (case1 ())
@@ -152,6 +152,9 @@
            lemma : {x : OD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z
            lemma {x} {z} d = def-subst d oiso refl
 
+=-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
+=-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso)
+
 ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
    lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
@@ -226,6 +229,11 @@
 ... | min with eq→ ( def-subst (o<→c< (Minimumo.min<x min)) oiso refl )
 ... | ()
        
+∅0 : {n : Level} →  { x : Ordinal {n} } → o∅ {n} o< x → ¬ ( ord→od x  == od∅ {n} )
+∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt
+... | min with eq→ (o<→c< (Minimumo.min<x min))
+... | ()
+       
 
 is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
 is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
@@ -240,10 +248,15 @@
 is-∋ {n} x y | tri≈ ¬a b ¬c = no ¬c
 is-∋ {n} x y | tri> ¬a ¬b c = yes c
 
+is-o∅ : {n : Level} →  ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
+is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
+is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
+is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
+
 open _∧_
 
-∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
-∅9 x not = ∅5 ( od→ord x) lemma where
+∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x
+∅9 {_} {x} not = ∅5  lemma where
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7  eq )
 
@@ -319,43 +332,46 @@
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
          minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
-         minord x not = ominimal (od→ord x) (∅9 x not)
+         minord x not = ominimal (od→ord x) (∅9 not)
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
          minimul x  not = ord→od ( mino (minord x not))
          minimul<x : (x : OD {suc n} ) →  (not :  ¬ x == od∅ ) → x ∋ minimul x not
          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 {suc 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₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-         proj1 ( regularity x non ) =  minimul<x x non 
-         proj2 ( regularity x non ) = reg1 where
-            reg2 : {y : Ordinal} → ( def (minimul x non) y ∧ (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 
+         regularity-ord :  (x : Ordinal ) (not :  o∅ o< x ) →
+            (ord→od x ∋ minimul (ord→od x) (∅0 not)) ∧ (Select (minimul (ord→od x) (∅0 not)) (λ x₁ → (minimul (ord→od x) (∅0 not) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
+         proj1 ( regularity-ord x non ) =  minimul<x (ord→od x) (∅0 non) 
+         proj2 ( regularity-ord x non ) = reg1 where
+            reg2 : {y : Ordinal} → ( def (minimul (ord→od x) (∅0 non)) y ∧ (minimul (ord→od x) (∅0 non) ∋ ord→od y) ∧ ((ord→od x) ∋ ord→od y) ) → ⊥ 
             reg2 {y} t with proj1 t | proj1 (proj2 t) | proj2 (proj2 t)
-            ... | p1 | p2 | p3  with is-∋ x ( ord→od y)
+            ... | p1 | p2 | p3  with is-∋ (ord→od x) ( ord→od y)
             reg2 {y} t | p1 | p2 | p3 | no ¬p = ⊥-elim (¬p p3 )                         --  ¬ x ∋ ord→od y     empty x case
-            reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul x non) (ord→od y)
+            reg2 {y} t | p1 | p2 | p3 | yes p with is-∋ (minimul (ord→od x) (∅0 non)) (ord→od y)
             reg2 {y} t | p1 | p2 | p3 | yes p | no ¬p = ⊥-elim (¬p p2 )                 --  minimum contains nothing q.e.d.
             reg2 {y} t | p1 | p2 | p3 | yes p | yes p₁ = {!!}
-            reg0 : {y : Ordinal {suc 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 trio< y (mino (minord x non)) 
-            reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} ( record {
-                    proj1 = (def-subst {suc n} {minimul x  non} (o<→c< a) refl diso ) 
-                  ; proj2 = record { proj1 = proj1 (proj2 t )
-                  ; proj2 = proj2 (proj2 t )
-                 }} ) 
+            reg0 : {y : Ordinal {suc n}} → Minimumo x → def (Select (minimul (ord→od x) (∅0 non)) (λ z → (minimul (ord→od x) (∅0 non) ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
+            reg0 {y} m t with trio< y (mino (minord (ord→od x) (∅0 non))) 
+            reg0 {y} m t | tri< a ¬b ¬c with reg2 {y} t 
             ... | ()
-            reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord x non) ) refl
-                     (def-subst {suc n} {ord→od y} {mino (minord x  non)} (proj1 t) refl (sym diso))
+            reg0 {y} m t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) (∅0 non)) ) refl
+                     (def-subst {suc n} {ord→od y} {mino (minord (ord→od x)  (∅0 non))} (proj1 t) refl (sym diso))
                   where
                lemma : ( ox oy : Ordinal {suc n} ) → ox ≡ oy  → ord→od ox c< ord→od oy  → Lift (suc n) ⊥
                lemma ox oy refl lt =  lift ( o≡→¬c< {suc n} {ord→od oy} {ord→od  oy} refl lt )
-            reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord x non)) (lemma (proj1 t)) c where
-                lemma : def (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq)))))) y → y o< mino (minord x non)
-                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord x non))} 
-                         (def-subst {suc n}  {ord→od (mino (minord x non))} {y} d refl (sym diso))
+            reg0 {y} m t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) (∅0 non))) (lemma {!!}) c where
+                lemma : def (ord→od (mino (ominimal x (∅5 (λ eq → (∅0 non) (∅7 {!!})))))) y → y o< mino (minord (ord→od x) (∅0 non))
+                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) (∅0 non)))} 
+                         (def-subst {suc n}  {ord→od (mino (minord (ord→od x) (∅0 non)))} {y} {!!} refl (sym diso))
                 lemma d | clt = o<-subst clt ord-iso ord-iso
             ... | ()
-            reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
-            reg1 = record { eq→ =  reg0 (minord x non) ; eq← = λ () }
+            reg1 :  Select (minimul (ord→od x) (∅0 non)) (λ x₁ → (minimul (ord→od x) (∅0 non) ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
+            reg1 = record { eq→ =  reg0 (ominimal x non) ; eq← = λ () } where
+         ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
+         ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  where
+         regularity :  (x : OD) (not : ¬ (x == od∅)) →
+            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+         regularity x not with regularity-ord ( od→ord x ) ( ∅9 not )
+         ... | t = ?
+