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

comparison ordinal-definable.agda @ 94:4659a815b70d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 08 Jun 2019 13:18:10 +0900
parents d382a7902f5e
children f3da2c87cee0
comparison
equal deleted inserted replaced
93:d382a7902f5e 94:4659a815b70d
134 lemma ox ox refl = eq-refl 134 lemma ox ox refl = eq-refl
135 135
136 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y 136 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y
137 o≡→== {n} {x} {.x} refl = eq-refl 137 o≡→== {n} {x} {.x} refl = eq-refl
138 138
139
140 =→¬< : {x : Nat } → ¬ ( x < x )
141 =→¬< {Zero} ()
142 =→¬< {Suc x} (s≤s lt) = =→¬< lt
143
144 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) 139 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
145 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x 140 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
146 141
147 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x 142 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x
148 c≤-refl x = case1 refl 143 c≤-refl x = case1 refl
149
150 o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy → ox o< oy → ⊥
151 o<¬≡ ox ox refl (case1 lt) = =→¬< lt
152 o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
153 144
154 o<→o> : {n : Level} → { x y : OD {n} } → (x == y) → (od→ord x ) o< ( od→ord y) → ⊥ 145 o<→o> : {n : Level} → { x y : OD {n} } → (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
155 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with 146 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
156 yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case1 lt )) oiso diso ) 147 yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case1 lt )) oiso diso )
157 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx ) 148 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
186 o<∋→ : {n : Level} → { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x 177 o<∋→ : {n : Level} → { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x
187 o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso diso t where 178 o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso diso t where
188 t : def (ord→od (od→ord a)) (od→ord (ord→od (od→ord x))) 179 t : def (ord→od (od→ord a)) (od→ord (ord→od (od→ord x)))
189 t = o<→c< {suc n} {od→ord x} {od→ord a} lt 180 t = o<→c< {suc n} {od→ord x} {od→ord a} lt
190 181
191 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
192 ¬x<0 {n} {x} (case1 ())
193 ¬x<0 {n} {x} (case2 ())
194
195 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 182 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
196 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} )) 183 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
197 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where 184 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
198 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥ 185 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
199 lemma lt with def-subst (o<→c< lt) oiso refl 186 lemma lt with def-subst (o<→c< lt) oiso refl
254 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅ 241 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
255 lemma o∅ ne | yes refl | () 242 lemma o∅ ne | yes refl | ()
256 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p)) 243 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))
257 244
258 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 245 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
259 246 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
260 postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) 247
248 Def : OD {suc n} → OD {suc n}
249 Def X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x }
261 250
262 251
263 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 252 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
264 OD→ZF {n} = record { 253 OD→ZF {n} = record {
265 ZFSet = OD {suc n} 254 ZFSet = OD {suc n}
282 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } 271 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
283 Union : OD {suc n} → OD {suc n} 272 Union : OD {suc n} → OD {suc n}
284 Union U = record { def = λ y → osuc y o< (od→ord U) } 273 Union U = record { def = λ y → osuc y o< (od→ord U) }
285 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 274 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
286 Power : OD {suc n} → OD {suc n} 275 Power : OD {suc n} → OD {suc n}
287 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x } 276 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def (ord→od y) x → def X x }
288 ZFSet = OD {suc n} 277 ZFSet = OD {suc n}
289 _∈_ : ( A B : ZFSet ) → Set (suc n) 278 _∈_ : ( A B : ZFSet ) → Set (suc n)
290 A ∈ B = B ∋ A 279 A ∈ B = B ∋ A
291 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 280 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
292 _⊆_ A B {x} = A ∋ x → B ∋ x 281 _⊆_ A B {x} = A ∋ x → B ∋ x
320 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 309 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
321 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 310 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
322 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 311 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
323 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 312 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
324 empty x () 313 empty x ()
325 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x } 314 --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def X x }
326 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 315 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
327 power→ A t P∋t {x} t∋x = {!!} 316 power→ A t P∋t {x} t∋x = ?
328 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 317 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
329 power← A t t→A z = {!!} 318 power← A t t→A z _ = ?
330 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} 319 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
331 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) 320 union-u X z U>z = ord→od ( osuc ( od→ord z ) )
332 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z 321 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z
333 union-lemma-u {X} {z} U>z = lemma <-osuc where 322 union-lemma-u {X} {z} U>z = lemma <-osuc where
334 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz 323 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz