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

comparison OD.agda @ 318:9e0c97ab3a4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace max
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Jul 2020 18:49:05 +0900
parents 57df07b63cae
children eef432aa8dfb
comparison
equal deleted inserted replaced
317:57df07b63cae 318:9e0c97ab3a4a
207 207
208 208
209 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 209 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
210 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 210 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
211 211
212 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → HOD 212 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
213 in-codomain X ψ = record { od = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } ; odmax = {!!} ; <odmax = {!!} } 213 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
214 214
215 -- Power Set of X ( or constructible by λ y → odef X (od→ord y ) 215 -- Power Set of X ( or constructible by λ y → odef X (od→ord y )
216 216
217 ZFSubset : (A x : HOD ) → HOD 217 ZFSubset : (A x : HOD ) → HOD
218 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set 218 ZFSubset A x = record { od = record { def = λ y → odef A y ∧ odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma } where -- roughly x = A → Set
264 } where 264 } where
265 ZFSet = HOD -- is less than Ords because of maxod 265 ZFSet = HOD -- is less than Ords because of maxod
266 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 266 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
267 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 267 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
268 Replace : HOD → (HOD → HOD) → HOD 268 Replace : HOD → (HOD → HOD) → HOD
269 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x)) 269 Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
270 ; odmax = rmax ; <odmax = rmax<} where
271 rmax : Ordinal
272 rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
273 rmax< : {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
274 rmax< lt = proj1 lt
270 _∩_ : ( A B : ZFSet ) → ZFSet 275 _∩_ : ( A B : ZFSet ) → ZFSet
271 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 }
277 ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
272 Union : HOD → HOD 278 Union : HOD → HOD
273 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) } ; odmax = {!!} ; <odmax = {!!} } 279 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x))) }
280 ; odmax = osuc (od→ord U) ; <odmax = umax< } where
281 umax< : {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
282 umax< {y} not = {!!}
274 _∈_ : ( A B : ZFSet ) → Set n 283 _∈_ : ( A B : ZFSet ) → Set n
275 A ∈ B = B ∋ A 284 A ∈ B = B ∋ A
276 285
277 OPwr : (A : HOD ) → HOD 286 OPwr : (A : HOD ) → HOD
278 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) 287 OPwr A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
354 } 363 }
355 sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) 364 sup-c< : (ψ : HOD → HOD) → {X x : HOD} → X ∋ x → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
356 sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt ) 365 sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
357 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x 366 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x
358 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where 367 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {X} {x} lt ; proj2 = lemma } where
359 lemma : odef (in-codomain X ψ) (od→ord (ψ x)) 368 lemma : def (in-codomain X ψ) (od→ord (ψ x))
360 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 369 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
361 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y)) 370 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
362 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 371 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
363 lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y)))) 372 lemma2 : ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
364 → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y))) 373 → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
487 lemmaj : od→ord t o< od→ord (Ord (od→ord A)) 496 lemmaj : od→ord t o< od→ord (Ord (od→ord A))
488 lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt 497 lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt
489 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) 498 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
490 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) 499 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))))
491 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) 500 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
492 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) 501 lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
493 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 502 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
494 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 503 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
495 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A ))) 504 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A )))
496 505
497 506