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

comparison ordinal-definable.agda @ 93:d382a7902f5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replacement
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jun 2019 09:36:41 +0900
parents b4742cf4ef97
children 4659a815b70d
comparison
equal deleted inserted replaced
92:ef0dfc4b97fd 93:d382a7902f5e
282 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } 282 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
283 Union : OD {suc n} → OD {suc n} 283 Union : OD {suc n} → OD {suc n}
284 Union U = record { def = λ y → osuc y o< (od→ord U) } 284 Union U = record { def = λ y → osuc y o< (od→ord U) }
285 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 285 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
286 Power : OD {suc n} → OD {suc n} 286 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 ) } 287 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x }
288 ZFSet = OD {suc n} 288 ZFSet = OD {suc n}
289 _∈_ : ( A B : ZFSet ) → Set (suc n) 289 _∈_ : ( A B : ZFSet ) → Set (suc n)
290 A ∈ B = B ∋ A 290 A ∈ B = B ∋ A
291 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 291 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
292 _⊆_ A B {x} = A ∋ x → B ∋ x 292 _⊆_ A B {x} = A ∋ x → B ∋ x
309 ; power← = power← 309 ; power← = power←
310 ; extensionality = extensionality 310 ; extensionality = extensionality
311 ; minimul = minimul 311 ; minimul = minimul
312 ; regularity = regularity 312 ; regularity = regularity
313 ; infinity∅ = infinity∅ 313 ; infinity∅ = infinity∅
314 ; infinity = {!!} 314 ; infinity = λ _ → infinity
315 ; selection = λ {ψ} {X} {y} → selection {ψ} {X} {y} 315 ; selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
316 ; replacement = {!!} 316 ; replacement = replacement
317 } where 317 } where
318 open _∧_ 318 open _∧_
319 open Minimumo 319 open Minimumo
320 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 320 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) 321 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) 322 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
323 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 323 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
324 empty x () 324 empty x ()
325 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } 325 --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x }
326 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 326 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
327 power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) ) 327 power→ A t P∋t {x} t∋x = {!!}
328 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 328 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
329 power← A t t→A z = record { proj1 = lemma2 ; proj2 = lemma1 } where 329 power← A t t→A z = {!!}
330 lemma1 : def (ord→od (od→ord t)) z
331 lemma1 = {!!}
332 lemma2 : def A z
333 lemma2 = {!!}
334 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} 330 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
335 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) 331 union-u X z U>z = ord→od ( osuc ( od→ord z ) )
336 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z 332 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z
337 union-lemma-u {X} {z} U>z = lemma <-osuc where 333 union-lemma-u {X} {z} U>z = lemma <-osuc where
338 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz 334 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
352 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 348 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
353 selection {ψ} {X} {y} = record { 349 selection {ψ} {X} {y} = record {
354 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 350 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
355 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 351 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
356 } 352 }
353 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
354 replacement {ψ} X x = sup-c< ψ {x}
357 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 355 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
358 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 356 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
359 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 357 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
360 minimul x not = od∅ 358 minimul x not = od∅
361 regularity : (x : OD) (not : ¬ (x == od∅)) → 359 regularity : (x : OD) (not : ¬ (x == od∅)) →
408 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n) 406 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
409 lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ())) 407 lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
410 lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ())) 408 lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
411 lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2 409 lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
412 lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl 410 lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
413 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x 411
414 replacement {ψ} X x = {!!}
415