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

comparison HOD.agda @ 135:b60b6e8a57b0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
otrans in repl
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 00:51:12 +0900
parents b52683497a27
children 3cc848664a86
comparison
equal deleted inserted replaced
134:b52683497a27 135:b60b6e8a57b0
232 232
233 csuc : {n : Level} → HOD {suc n} → HOD {suc n} 233 csuc : {n : Level} → HOD {suc n} → HOD {suc n}
234 csuc x = Ord ( osuc ( od→ord x )) 234 csuc x = Ord ( osuc ( od→ord x ))
235 235
236 in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n} 236 in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
237 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y ))))) } 237 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y )))))
238 ; otrans = lemma } where
239 lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
240 {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
241 lemma {x} notx {y} y<x noty = {!!}
238 242
239 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 243 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
240 244
241 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n} 245 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
242 ZFSubset A x = record { def = λ y → def A y ∧ def x y ; otrans = lemma } where 246 ZFSubset A x = record { def = λ y → def A y ∧ def x y ; otrans = lemma } where
297 ; Replace = Replace 301 ; Replace = Replace
298 ; infinite = Ord omega 302 ; infinite = Ord omega
299 ; isZF = isZF 303 ; isZF = isZF
300 } where 304 } where
301 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} 305 Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
302 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 306 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ;
307 otrans = lemma } where
308 lemma : {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x →
309 {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y
310 lemma {x} repl {y} y<x = record { proj1 = ordtrans y<x (proj1 repl)
311 ; proj2 = otrans (in-codomain X ψ) (proj2 repl) y<x }
303 Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n} 312 Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
304 Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x ) ; otrans = lemma } where 313 Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x ) ; otrans = lemma } where
305 lemma : {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) → 314 lemma : {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
306 {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y) 315 {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
307 lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where 316 lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
343 ; minimul = minimul 352 ; minimul = minimul
344 ; regularity = regularity 353 ; regularity = regularity
345 ; infinity∅ = infinity∅ 354 ; infinity∅ = infinity∅
346 ; infinity = λ _ → infinity 355 ; infinity = λ _ → infinity
347 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} 356 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
348 ; replacement← = {!!} 357 ; replacement← = replacement←
349 ; replacement→ = {!!} 358 ; replacement→ = replacement→
350 } where 359 } where
351 360
352 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 361 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
353 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 362 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
354 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 363 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
416 425
417 -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 426 -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
418 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x 427 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
419 power→ = {!!} 428 power→ = {!!}
420 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 429 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
421 power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} {!!} {!!} lemma1 where 430 power← A t t→A = {!!} where
422 a = od→ord A 431 a = od→ord A
423 ψ : HOD → HOD 432 ψ : HOD → HOD
424 ψ y = Def (Ord a) ∩ y 433 ψ y = Def (Ord a) ∩ y
425 lemma1 : od→ord (Def (Ord a) ∩ t) ≡ od→ord t
426 lemma1 = {!!}
427 lemma2 : Ord ( sup-o ( λ x → od→ord (ψ (ord→od x )))) ≡ Power A
428 lemma2 = {!!}
429 434
430 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n} 435 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
431 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 436 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
432 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 437 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
433 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) 438 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))