comparison ordinal-definable.agda @ 42:4d5fc6381546

regurality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 May 2019 10:28:02 +0900
parents b60db5903f01
children 0d9b9db14361
comparison
equal deleted inserted replaced
41:b60db5903f01 42:4d5fc6381546
92 92
93 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where 93 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
94 field 94 field
95 mino : Ordinal {n} 95 mino : Ordinal {n}
96 min<x : mino o< x 96 min<x : mino o< x
97 defmin : def ( ord→od x ) mino
98 defmin = lemma ( o<→c< min<x ) where
99 lemma : def (ord→od x) (od→ord ( ord→od mino)) → def ( ord→od x ) mino
100 lemma m< = def-subst {n} {ord→od x} m< refl diso
101 97
102 ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x 98 ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x
103 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ()) 99 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
104 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ()) 100 ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
105 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ()) 101 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ())
227 minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x) 223 minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x)
228 minord x not = ominimal (od→ord x) (∅9 x not) 224 minord x not = ominimal (od→ord x) (∅9 x not)
229 minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} 225 minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n}
230 minimul x not = ord→od ( mino (minord x not)) 226 minimul x not = ord→od ( mino (minord x not))
231 minimul<x : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ minimul x not 227 minimul<x : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ minimul x not
232 minimul<x x not = lemma0 where 228 minimul<x x not = lemma0 (min<x (minord x not)) where
233 lemma : def x (mino (minord x not)) 229 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
234 lemma = def-subst (defmin (minord x not)) oiso refl 230 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
235 lemma0 : def x (od→ord (ord→od (mino (minord x not))))
236 lemma0 = def-subst {n} {x} lemma refl {!!}
237 regularity : (x : OD) → (not : ¬ x ≡ od∅ ) → 231 regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
238 Lift (suc n) (x ∋ minimul x not ) ∧ 232 Lift (suc n) (x ∋ minimul x not ) ∧
239 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅) 233 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
240 proj1 ( regularity x non ) = lift ( minimul<x x non ) 234 proj1 ( regularity x non ) = lift ( minimul<x x non )
241 proj2 ( regularity x non ) = {!!} 235 proj2 ( regularity x non ) = cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) ) where
236 lemma : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z
237 lemma z with (minimul x non ∋ (ord→od z)) | x ∋ (ord→od z)
238 ... | s | t = {!!}
239 lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z ≡ Lift n ⊥
240 lemma0 = {!!}
241