Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal-definable.agda @ 70:cd9cf8b09610
Union needs +1 space
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 01 Jun 2019 10:01:38 +0900 |
parents | 93abc0133b8a |
children | d088eb66564e |
comparison
equal
deleted
inserted
replaced
69:93abc0133b8a | 70:cd9cf8b09610 |
---|---|
330 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }) | 330 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }) |
331 isZF = record { | 331 isZF = record { |
332 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } | 332 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } |
333 ; pair = pair | 333 ; pair = pair |
334 ; union-u = {!!} | 334 ; union-u = {!!} |
335 ; union-iso = {!!} | 335 ; union→ = {!!} |
336 ; union← = {!!} | |
336 ; empty = empty | 337 ; empty = empty |
337 ; power→ = {!!} | 338 ; power→ = {!!} |
338 ; power← = {!!} | 339 ; power← = {!!} |
339 ; extensionality = {!!} | 340 ; extensionality = {!!} |
340 ; minimul = minimul | 341 ; minimul = minimul |
349 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) | 350 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) |
350 proj1 (pair A B ) = case1 refl | 351 proj1 (pair A B ) = case1 refl |
351 proj2 (pair A B ) = case2 refl | 352 proj2 (pair A B ) = case2 refl |
352 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) | 353 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) |
353 empty x () | 354 empty x () |
355 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} | |
356 union-u X z U>z with od→ord X | od→ord z | |
357 union-u X z (case1 (s≤s x)) | record { lv = Suc lX ; ord = oX } | record { lv = lz ; ord = oz } = ord→od (mid (Suc lX) lz oX oz (s≤s x) ) where | |
358 mid : (lX lz : Nat) → (oX : OrdinalD {suc n} lX ) → (oz : OrdinalD {suc n} lz ) → lX > lz → Ordinal {suc n} | |
359 mid (Suc lX) 0 oX oz (s≤s z≤n) = record { lv = 0 ; ord = OSuc 0 oz } | |
360 mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (Φ (Suc lz)) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (Φ (Suc lz) ) } | |
361 mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (OSuc (Suc lz) oz) (s≤s (s≤s lt)) = record { lv = Suc lz ; ord = OSuc (Suc lz) (OSuc (Suc lz) oz) } | |
362 mid (Suc (Suc lX)) (Suc lz) (Φ (Suc (Suc lX))) (ℵ lz) (s≤s (s≤s lt)) = record { lv = (Suc (Suc lX)) ; ord = OSuc (Suc (Suc lX)) (ℵ (Suc lX)) } | |
363 mid (Suc (Suc lX)) (Suc lz) (OSuc (Suc (Suc lX)) oX) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = oX } | |
364 mid (Suc (Suc lX)) (Suc lz) (ℵ (Suc lX)) oz (s≤s (s≤s lt)) = record { lv = Suc (Suc lX) ; ord = OSuc (Suc (Suc lX)) (Φ (Suc (Suc lX))) } | |
365 union-u X z (case2 Φ<) | record { lv = Zero ; ord = (OSuc 0 oX) } | record { lv = .0 ; ord = .(Φ 0) } = | |
366 ord→od (record { lv = Zero ; ord = oX }) -- this case contains X = odΦ | |
367 union-u X z (case2 Φ<) | record { lv = Suc lv₁ ; ord = (OSuc (Suc lv₁) oX) } | record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) } = ord→od (record { lv = Suc lv₁ ; ord = oX } ) | |
368 union-u X z (case2 (s< x)) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(OSuc lv₁ _) } = {!!} | |
369 union-u X z (case2 ℵΦ<) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } = ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (Φ (Suc lX))} ) | |
370 union-u X z (case2 (ℵ< x)) | record { lv = Suc lX ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = OSuc (Suc _) oz } = | |
371 ord→od ( record { lv = Suc lX ; ord = OSuc (Suc lX ) (OSuc (Suc lX) (OSuc (Suc lX) oz ))} ) | |
372 union-u X z (case2 ℵs<) | record { lv = Suc lX ; ord = OSuc (Suc lX) (ℵ lX) } | record { lv = Suc lX ; ord = ℵ lX } = {!!} | |
373 union-u X z (case2 (ℵss< x)) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!} | |
354 union→ : (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y | 374 union→ : (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y |
355 union→ X x y X∋x x∋y = c<→o< (transitive {n} {X} {x} {y} X∋x x∋y ) | 375 union→ X x y X∋x x∋y = c<→o< (transitive {n} {X} {x} {y} X∋x x∋y ) |
356 union-u : (X z : OD {suc n}) → OD {suc n} | 376 union← : (X z : OD {suc n}) → (X∋z : Union X ∋ z) → ((Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z)) |
357 union-u X z = record { def = ( λ u → (u o< od→ord X) ∧ (od→ord z o< u) ) } | 377 union← = {!!} |
358 union-iso : (X z : OD {suc n}) → (Union X ∋ z) ⇔ ((Union X ∋ union-u X z ) ∧ (union-u X z ∋ z)) | |
359 -- ((x : OD) → (z ∋ x → y ∋ x)) → y ∋ z | |
360 proj1 ( union-iso X z ) U∋z = record { proj1 = U∋u ; proj2 = u∋z } where | |
361 U∋u : Union X ∋ union-u X z | |
362 U∋u = {!!} | |
363 u∋z : union-u X z ∋ z | |
364 u∋z = {!!} | |
365 proj2 (union-iso X z ) U∋u∧U∋z = transitive {n} {!!} {!!} -- (proj1 U∋u∧U∋z ) (proj2 U∋u∧U∋z ) | |
366 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y | 378 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y |
367 ψiso {ψ} t refl = t | 379 ψiso {ψ} t refl = t |
368 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) | 380 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) |
369 selection {ψ} {X} {y} = record { | 381 selection {ψ} {X} {y} = record { |
370 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } | 382 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } |