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

comparison OD.agda @ 310:73a2a8ec9603

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 Tue, 30 Jun 2020 08:55:12 +0900
parents d4802179a66f
children bf01e924e62e
comparison
equal deleted inserted replaced
309:d4802179a66f 310:73a2a8ec9603
218 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x) 218 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
219 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and)) 219 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
220 220
221 221
222 OPwr : (A : HOD ) → HOD 222 OPwr : (A : HOD ) → HOD
223 OPwr A = Ord ( sup-o A {!!} ) -- ( λ x → od→ord ( ZFSubset A x) ) ) 223 OPwr A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
224 224
225 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n 225 -- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n
226 -- _⊆_ A B {x} = A ∋ x → B ∋ x 226 -- _⊆_ A B {x} = A ∋ x → B ∋ x
227 227
228 record _⊆_ ( A B : HOD ) : Set (suc n) where 228 record _⊆_ ( A B : HOD ) : Set (suc n) where
268 ; isZF = isZF 268 ; isZF = isZF
269 } where 269 } where
270 ZFSet = HOD -- is less than Ords because of maxod 270 ZFSet = HOD -- is less than Ords because of maxod
271 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 271 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
272 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 272 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
273 Replace : HOD → (HOD → HOD ) → HOD 273 Replace : HOD → (HOD → HOD) → HOD
274 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X {!!} ) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x)) 274 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋x → od→ord (ψ (ord→od x)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
275 _∩_ : ( A B : ZFSet ) → ZFSet 275 _∩_ : ( A B : ZFSet ) → ZFSet
276 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))} 276 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
277 Union : HOD → HOD 277 Union : HOD → HOD
278 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} } 278 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} }
279 _∈_ : ( A B : ZFSet ) → Set n 279 _∈_ : ( A B : ZFSet ) → Set n
399 proj1 = odef-subst {_} {_} {(Ord a)} {z} 399 proj1 = odef-subst {_} {_} {(Ord a)} {z}
400 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 400 ( t→A (odef-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
401 lemma1 : {a : Ordinal } { t : HOD } 401 lemma1 : {a : Ordinal } { t : HOD }
402 → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 402 → (eq : ZFSubset (Ord a) t =h= t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
403 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 403 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
404 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) {!!} -- (λ x → od→ord (ZFSubset (Ord a) x)) 404 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
405 lemma = {!!} -- sup-o< 405 lemma = {!!} -- sup-o<
406 406
407 -- 407 --
408 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first 408 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
409 -- then replace of all elements of the Power set by A ∩ y 409 -- then replace of all elements of the Power set by A ∩ y
423 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 )) 423 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
424 lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x)) 424 lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) → ¬ ¬ (odef A (od→ord x))
425 lemma5 {y} eq not = (lemma3 (ord→od y) eq) not 425 lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
426 426
427 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 427 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
428 power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 428 power← A t t→A = record { proj1 = {!!} ; proj2 = lemma2 } where
429 a = od→ord A 429 a = od→ord A
430 lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x 430 lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
431 lemma0 {x} t∋x = c<→o< (t→A t∋x) 431 lemma0 {x} t∋x = c<→o< (t→A t∋x)
432 lemma3 : OPwr (Ord a) ∋ t 432 lemma3 : OPwr (Ord a) ∋ t
433 lemma3 = ord-power← a t lemma0 433 lemma3 = ord-power← a t lemma0
437 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 437 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
438 A ∩ t 438 A ∩ t
439 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 439 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
440 t 440 t
441 ∎ 441 ∎
442 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) {!!} -- (λ x → od→ord (A ∩ x)) 442 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
443 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) {!!}) -- (λ x → od→ord (A ∩ x))) 443 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))))
444 lemma4 {!!} -- (sup-o< {λ x → od→ord (A ∩ x)} ) 444 lemma4 {!!} -- (sup-o< {λ x → od→ord (A ∩ x)} )
445 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) 445 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
446 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 446 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
447 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 447 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
448 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 448 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))