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

comparison ordinal-definable.agda @ 70:cd9cf8b09610

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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) }