# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558653701 -32400
# Node ID b60db5903f01b9404a0e98b2ca21097931da87f6
# Parent  9439ff020cbd7890d9438fd4b4bcb222437c0b58
mnimul

diff -r 9439ff020cbd -r b60db5903f01 ordinal-definable.agda
--- a/ordinal-definable.agda	Thu May 23 20:24:15 2019 +0900
+++ b/ordinal-definable.agda	Fri May 24 08:21:41 2019 +0900
@@ -73,7 +73,7 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
    c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) }  )
-   ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)}))) 
+   ... | t with t (case2 (s< ℵΦ<   )) 
    c3 .(Suc lx) (ℵ lx) d not | t | ()
 
 -- find : {n : Level} → ( x : Ordinal {n} ) → o∅ o< x → Ordinal {n}  
@@ -90,16 +90,25 @@
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
    lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
 
-ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Ordinal {n}
+record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
+  field
+     mino : Ordinal {n}
+     min<x :  mino o< x
+  defmin : def ( ord→od x ) mino
+  defmin = lemma ( o<→c< min<x ) where
+     lemma : def (ord→od x) (od→ord ( ord→od mino))  → def ( ord→od x ) mino
+     lemma m< = def-subst {n} {ord→od x} m< refl diso
+
+ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x
 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ())
-ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { lv = Zero ; ord = Φ 0 }
-ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< }
+ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { mino = record { lv = lv ; ord = Φ lv } ; min<x = case1 (s≤s ≤-refl)}
 ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { lv = (Suc lv) ; ord = ord }
+ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl}
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lv ; ord = Φ (Suc lv) } ; min<x = case2 ℵΦ<  }
 ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ())
 
 ∅4 : {n : Level} →  ( x : OD {n} )  →  x  ≡ od∅ {n}  → od→ord x ≡ o∅ {n}
@@ -205,6 +214,7 @@
        ;   replacement = {!!}
      } where
          open _∧_ 
+         open Minimumo
          pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B)
          proj1 (pair A B ) = lift ( case1 refl )
          proj2 (pair A B ) = lift ( case2 refl )
@@ -214,10 +224,18 @@
          union→ X x y (lift X∋x) (lift x∋y) = lift {!!}  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
+         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} 
-         minimul x  not = ord→od ( ominimal (od→ord x) (∅9 x not) )
+         minimul x  not = ord→od ( mino (minord x not))
+         minimul<x : (x : OD {n} ) →  (not :  ¬ x ≡ od∅ ) → x ∋ minimul x not
+         minimul<x x not = lemma0 where
+            lemma :  def x (mino (minord x not))
+            lemma = def-subst (defmin (minord x not)) oiso refl
+            lemma0 : def x (od→ord (ord→od (mino (minord x not))))
+            lemma0 = def-subst {n} {x} lemma refl {!!}
          regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
                 Lift (suc n) (x ∋ minimul x not ) ∧
                 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
-         proj1 ( regularity x non ) = {!!}
+         proj1 ( regularity x non ) = lift ( minimul<x x non )
          proj2 ( regularity x non ) = {!!}
diff -r 9439ff020cbd -r b60db5903f01 ordinal.agda
--- a/ordinal.agda	Thu May 23 20:24:15 2019 +0900
+++ b/ordinal.agda	Fri May 24 08:21:41 2019 +0900
@@ -25,7 +25,7 @@
 data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
    Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
    s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
-   ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } →  Φ  (Suc lx) d< (ℵ lx) 
+   ℵΦ< : {lx : Nat} → Φ  (Suc lx) d< (ℵ lx) 
    ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x  →  OSuc  (Suc lx) x d< (ℵ lx) 
    ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx)
    ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x 
@@ -88,8 +88,8 @@
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
-triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  (ℵΦ<  {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
-triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ<  {_} {lv} {Φ (Suc lv)} )
+triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  ℵΦ<  (λ ()) ( λ lt → trio<> lt ℵΦ<) 
+triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ<  
 triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y
 triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) )
 triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri<  ℵs< (λ ()) ( λ lt → trio<> lt  ℵs< )
@@ -122,17 +122,17 @@
 
 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
-orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< {_} {lx} {y}
+orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< 
 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
 orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ)
 orddtrans ℵs< (ℵ< ())
 orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t )
 orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ<
-orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s< ( ℵΦ< {_} {_} {ℵ k} )
+orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s<  ℵΦ< 
 orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t )
 orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs<
 orddtrans ℵΦ< (ℵss< y<z) = Φ<
-orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans (ℵΦ< {_} {_} {k})  y<z)
+orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ<   y<z)
 orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) 
 orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) 
 orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z )