# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559099203 -32400
# Node ID 6a1f67a4cc6e9fb5bca7a8cbdc5c0bc34620ec93
# Parent  d13d1351a1face0834e5e81a71215ae58a7807df
dead end

diff -r d13d1351a1fa -r 6a1f67a4cc6e ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 05:46:05 2019 +0900
+++ b/ordinal-definable.agda	Wed May 29 12:06:43 2019 +0900
@@ -70,6 +70,9 @@
   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})
 
+congf : {n : Level} {x y : OD {n}} → { f g : OD {n} → OD {n} } → x ≡ y → f ≡ g → f x ≡ g y 
+congf refl refl = refl
+
 o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
 o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
 
@@ -233,6 +236,10 @@
 ∅0 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal x lt
 ... | min with eq→ (o<→c< (Minimumo.min<x min))
 ... | ()
+
+∅< : {n : Level} →  { x y : OD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
+∅< {n} {x} {y} d eq with eq→ eq d
+∅< {n} {x} {y} d eq | lift ()
        
 
 is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
@@ -260,6 +267,9 @@
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7  eq )
 
+∅10 : {n : Level} →  {ox : Ordinal {n}} → {x : OD{n}} → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅)) → o∅ o< ox
+∅10 {n} {ox} {x} refl not = subst (λ k → o∅ o< k) diso (∅9 not)
+
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
@@ -333,6 +343,8 @@
               proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
+         ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
+         ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
          minord x not = ominimal (od→ord x) (∅9 not)
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
@@ -341,46 +353,31 @@
          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-ord :  (x : Ordinal ) (not :  ¬ (ord→od x == od∅)) →
-            (ord→od x ∋ minimul (ord→od x) not) ∧ (Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅)
-         proj1 ( regularity-ord x not ) =  minimul<x (ord→od x) not 
-         proj2 ( regularity-ord x not ) = reg1 where
-            reg2 : {y : Ordinal} → ( def (minimul (ord→od x) not) y ∧ (minimul (ord→od x) not ∋ 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-∋ (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 (ord→od x) not) (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}} → def (Select (minimul (ord→od x) not) (λ z → (minimul (ord→od x) not ∋ z) ∧ ((ord→od x) ∋ z))) y → def od∅ y
-            reg0 {y} t with trio< y (mino (minord (ord→od x) not)) 
-            reg0 {y} t | tri< a ¬b ¬c with reg2 {y} t 
-            ... | ()
-            reg0 {y} t | tri≈ ¬a refl ¬c = lemma y ( mino (minord (ord→od x) not) ) refl
-                     (def-subst {suc n} {ord→od y} {mino (minord (ord→od x)  not)} (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} t | tri> ¬a ¬b c with o<> y (mino (minord (ord→od x) not)) (lemma {!!}) c where
-                lemma : def (ord→od (mino (minord (ord→od x)  not))) y → y o< mino (minord (ord→od x) not)
-                lemma d with c<→o< {suc n} {ord→od y} {ord→od (mino (minord (ord→od x) not))} 
-                         (def-subst {suc n}  {ord→od (mino (minord (ord→od x) not))} {y} {!!} refl (sym diso))
-                lemma d | clt = o<-subst clt ord-iso ord-iso
-            ... | ()
-            reg1 :  Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅
-            reg1 = record { eq→ = reg0  ; eq← = λ () } where
-         ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
-         ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          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 =  
-             subst₂ ( λ x min  → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) )
-                              oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where
-                 lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not
-                 lemma = cong₂ (λ x not → minimul x not ) oiso {!!}
- 
-
-
-
-
-
+         regularity x not = regularity-ord (od→ord x) x (sym oiso ) not where
+             regularity-ord : (ox : Ordinal ) → (x : OD) → ( x ≡ ord→od ox ) → (not : ¬ (x == od∅))
+                  → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+             regularity-ord ox x refl not  = record { proj1 = minimul<x x not ; proj2 = record {eq→ = reg0 ; eq← = λ () } } where
+               noto : o∅ o< (od→ord (ord→od ox)) 
+               noto = lemma {ox} {od→ord (ord→od ox)} diso (∅10 refl not) where
+                  lemma : { ox oy : Ordinal {suc n}} → oy ≡ ox → o∅ o< ox → o∅ o< oy
+                  lemma refl lt = lt
+               Min : Minimumo ox 
+               Min = ominimal ox (∅10 refl not)
+               Mino : Minimumo (od→ord (ord→od ox )) 
+               Mino = ominimal (od→ord (ord→od ox )) noto
+               m=mo : ox ≡ od→ord (ord→od ox ) → mino Mino ≡ mino Min
+               m=mo eq with ox
+               ... | xx = ?
+               reg0 : {y : Ordinal {suc n}} → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) y → def od∅ y
+               reg0 {y} t with  trio< y ( mino Mino )
+               reg0 {y} t | tri< a ¬b ¬c = {!!}
+               reg0 {y} t | tri≈ ¬a refl ¬c with  o≡→¬c< {suc n} {ord→od (mino Mino)} refl lemma where
+                   lemma : ord→od y c< ord→od (mino Mino)
+                   lemma = subst (λ k → k  c< ord→od (mino Mino) ) oiso {!!} -- (proj1 t)
+               reg0 {y} t | tri≈ ¬a b ¬c | ()
+               reg0 {y} t | tri> ¬a ¬b c with  o<> y (mino Mino) lemma c where
+                   lemma : y o< mino Mino
+                   lemma = {!!}
+               reg0 {y} t | tri> ¬a ¬b c | ()