Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison ordinal-definable.agda @ 44:fcac01485f32

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
od→lv : {n : Level} → OD {n} → Nat does not worked
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 May 2019 04:12:30 +0900
parents 0d9b9db14361
children 33860eb44e47
comparison
equal deleted inserted replaced
43:0d9b9db14361 44:fcac01485f32
22 def : (x : Ordinal {n} ) → Set n 22 def : (x : Ordinal {n} ) → Set n
23 23
24 open OD 24 open OD
25 open import Data.Unit 25 open import Data.Unit
26 26
27 open Ordinal
28
27 postulate 29 postulate
28 od→ord : {n : Level} → OD {n} → Ordinal {n} 30 od→lv : {n : Level} → OD {n} → Nat
31 od→d : {n : Level} → (x : OD {n}) → OrdinalD {n} (od→lv x )
29 ord→od : {n : Level} → Ordinal {n} → OD {n} 32 ord→od : {n : Level} → Ordinal {n} → OD {n}
33
34 od→ord : {n : Level} → OD {n} → Ordinal {n}
35 od→ord x = record { lv = od→lv x ; ord = od→d x }
30 36
31 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 37 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
32 _∋_ {n} a x = def a ( od→ord x ) 38 _∋_ {n} a x = def a ( od→ord x )
33 39
34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n 40 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
124 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< } 130 ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< }
125 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)} 131 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)}
126 ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ()) 132 ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
127 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} 133 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}
128 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ()) 134 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
129 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 ℵΦ< } 135 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 ℵΦ< }
130 ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ()) 136 ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case2 ())
131 137
132 ∅4 : {n : Level} → ( x : OD {n} ) → x ≡ od∅ {n} → od→ord x ≡ o∅ {n} 138 ∅4 : {n : Level} → ( x : OD {n} ) → x ≡ od∅ {n} → od→ord x ≡ o∅ {n}
133 ∅4 {n} x refl = ∅3 lemma1 where 139 ∅4 {n} x refl = ∅3 lemma1 where
134 lemma0 : (y : Ordinal {n}) → def ( od∅ {n} ) y → ⊥ 140 lemma0 : (y : Ordinal {n}) → def ( od∅ {n} ) y → ⊥
135 lemma0 y (lift ()) 141 lemma0 y (lift ())
154 ∅8 {n} x (case2 ()) 160 ∅8 {n} x (case2 ())
155 161
156 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅ 162 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅
157 -- ∅10 {n} x not = ? 163 -- ∅10 {n} x not = ?
158 164
159 open Ordinal
160
161 -- ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y 165 -- ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y
162 -- ∋-subst refl refl x = x 166 -- ∋-subst refl refl x = x
163 167
164 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) 168 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x )
165 -- ∅77 {n} x lt = {!!} where 169 -- ∅77 {n} x lt = {!!} where
166 170
167 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} 171 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
168 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where 172 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where
173
174 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
175
176
177 ∅7'' : {n : Level} → ( x : OD {n} ) → od→lv {n} x ≡ Zero → od→d {n} x ≅ Φ {n} Zero → x == od∅ {n}
178 ∅7'' {n} x eq eq1 = {!!}
169 179
170 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n} 180 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n}
171 ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where 181 ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where
172 e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y 182 e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y
173 e0 {y} (case1 ()) 183 e0 {y} (case1 ())
174 e0 {y} (case2 ()) 184 e0 {y} (case2 ())
175 e1 : {y : Ordinal {n}} → def x y → def od∅ y 185 e1 : {y : Ordinal {n}} → def x y → def od∅ y
176 e1 {y} y<x = e0 ( o<-subst ( c<→o< {n} {x} y<x ) refl {!!} ) 186 e1 {y} y<x with c<→o< {n} {x} y<x
187 e1 {y} y<x | case1 lt = {!!}
188 e1 {y} y<x | case2 lt = {!!}
177 e2 : {y : Ordinal {n}} → def od∅ y → def x y 189 e2 : {y : Ordinal {n}} → def od∅ y → def x y
178 e2 {y} (lift ()) 190 e2 {y} (lift ())
179 191
180 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x 192 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
181 ∅9 x not = ∅5 ( od→ord x) lemma where 193 ∅9 x not = ∅5 ( od→ord x) lemma where
182 lemma : ¬ od→ord x ≡ o∅ 194 lemma : ¬ od→ord x ≡ o∅
183 lemma eq = not ( ∅7 x eq ) 195 lemma eq = not ( ∅7 x eq )
196
184 197
185 OD→ZF : {n : Level} → ZF {suc n} {n} 198 OD→ZF : {n : Level} → ZF {suc n} {n}
186 OD→ZF {n} = record { 199 OD→ZF {n} = record {
187 ZFSet = OD {n} 200 ZFSet = OD {n}
188 ; _∋_ = _∋_ 201 ; _∋_ = _∋_