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

comparison ordinal-definable.agda @ 69:93abc0133b8a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
union continue
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 May 2019 22:30:23 +0900
parents c69657d00557
children cd9cf8b09610
comparison
equal deleted inserted replaced
68:c69657d00557 69:93abc0133b8a
104 c3 .(Suc lx) (ℵ lx) d not | t | () 104 c3 .(Suc lx) (ℵ lx) d not | t | ()
105 105
106 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x 106 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x
107 def-subst df refl refl = df 107 def-subst df refl refl = df
108 108
109 transitive : {n : Level } { z y x : OD {n} } → z ∋ y → y ∋ x → z ∋ x 109 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z ∋ x
110 transitive {n} {z} {y} {x} z∋y x∋y with ordtrans ( c<→o< {n} {x} {y} x∋y ) ( c<→o< {n} {y} {z} z∋y ) 110 transitive {n} {z} {y} {x} z∋y x∋y with ordtrans ( c<→o< {suc n} {x} {y} x∋y ) ( c<→o< {suc n} {y} {z} z∋y )
111 ... | t = lemma0 (lemma t) where 111 ... | t = lemma0 (lemma t) where
112 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) 112 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
113 lemma xo<z = o<→c< xo<z 113 lemma xo<z = o<→c< xo<z
114 lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x) 114 lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x)
115 lemma0 dz = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso) 115 lemma0 dz = def-subst {suc n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
116 116
117 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where 117 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
118 field 118 field
119 mino : Ordinal {n} 119 mino : Ordinal {n}
120 min<x : mino o< x 120 min<x : mino o< x
277 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where 277 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
278 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ 278 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
279 lemma1 = cong ( λ k → od→ord k ) o∅→od∅ 279 lemma1 = cong ( λ k → od→ord k ) o∅→od∅
280 lemma o∅ ne | yes refl | () 280 lemma o∅ ne | yes refl | ()
281 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) 281 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))
282 282
283 -- ∃-set : {n : Level} → ( x : OD {suc n} ) → ( ψ : OD {suc n} → Set (suc n) ) → Set (suc n)
284 -- ∃-set = {!!}
283 285
284 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n )) 286 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n ))
285 287
286 -- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n} 288 -- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n}
287 -- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where 289 -- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where
308 Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n} 310 Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
309 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 311 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
310 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 312 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
311 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } 313 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
312 Union : OD {suc n} → OD {suc n} 314 Union : OD {suc n} → OD {suc n}
313 Union x = record { def = λ y → {z : Ordinal {suc n}} → def x z → def (ord→od z) y } 315 Union U = record { def = λ y → y o< (od→ord U) }
314 Power : OD {suc n} → OD {suc n} 316 Power : OD {suc n} → OD {suc n}
315 Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) } 317 Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) }
316 ZFSet = OD {suc n} 318 ZFSet = OD {suc n}
317 _∈_ : ( A B : ZFSet ) → Set (suc n) 319 _∈_ : ( A B : ZFSet ) → Set (suc n)
318 A ∈ B = B ∋ A 320 A ∈ B = B ∋ A
327 infixr 220 _⊆_ 329 infixr 220 _⊆_
328 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 } })
329 isZF = record { 331 isZF = record {
330 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 332 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
331 ; pair = pair 333 ; pair = pair
332 ; union→ = {!!} 334 ; union-u = {!!}
333 ; union← = {!!} 335 ; union-iso = {!!}
334 ; empty = empty 336 ; empty = empty
335 ; power→ = {!!} 337 ; power→ = {!!}
336 ; power← = {!!} 338 ; power← = {!!}
337 ; extensionality = {!!} 339 ; extensionality = {!!}
338 ; minimul = minimul 340 ; minimul = minimul
347 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 349 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
348 proj1 (pair A B ) = case1 refl 350 proj1 (pair A B ) = case1 refl
349 proj2 (pair A B ) = case2 refl 351 proj2 (pair A B ) = case2 refl
350 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 352 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
351 empty x () 353 empty x ()
352 union→ : (X x y : OD) → X ∋ x → x ∋ y → Union X ∋ y 354 union→ : (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
353 union→ X x y X∋x x∋y {z} X∋z = {!!} -- transitive {suc n} {X} {x} {y} X∋x x∋y 355 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}
357 union-u X z = record { def = ( λ u → (u o< od→ord X) ∧ (od→ord z o< u) ) }
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 )
354 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 366 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
355 ψiso {ψ} t refl = t 367 ψiso {ψ} t refl = t
356 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 368 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
357 selection {ψ} {X} {y} = record { 369 selection {ψ} {X} {y} = record {
358 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 370 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }