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

comparison HOD.agda @ 139:53077af367e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 22:23:02 +0900
parents 567084f2278f
children 312e27aa3cb5
comparison
equal deleted inserted replaced
138:567084f2278f 139:53077af367e9
300 lemma : {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) → 300 lemma : {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
301 {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y) 301 {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
302 lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where 302 lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
303 y<X : X ∋ ord→od y 303 y<X : X ∋ ord→od y
304 y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso) ) 304 y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso) )
305 in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
306 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y )))))
307 ; otrans = lemma } where
308 lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
309 {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
310 lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } ))
311 Replace' : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
312 Replace' X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧ ( x == ψ (Ord y) ))))
313 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}
314 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ; 306 Replace X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧ ( x == ψ (Ord y) ))))
315 otrans = lemma } where
316 lemma : {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x →
317 {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y
318 lemma {x} repl {y} y<x = record { proj1 = ordtrans y<x (proj1 repl)
319 ; proj2 = otrans (in-codomain X ψ) (proj2 repl) y<x }
320 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n} 307 _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
321 x , y = Ord (omax (od→ord x) (od→ord y)) 308 x , y = Ord (omax (od→ord x) (od→ord y))
322 Union : HOD {suc n} → HOD {suc n} 309 Union : HOD {suc n} → HOD {suc n}
323 Union U = cseq U 310 Union U = cseq U
324 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 311 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
454 ; proj2 = λ s → record { proj1 = λ y1 dy1 → 441 ; proj2 = λ s → record { proj1 = λ y1 dy1 →
455 subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso ))) 442 subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
456 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where 443 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
457 -- ψ< : {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} → ψ y ∋ x → ψ y' == x 444 -- ψ< : {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} → ψ y ∋ x → ψ y' == x
458 -- ψ< = {!!} 445 -- ψ< = {!!}
459 replacement←' : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace' X ψ ∋ ψ x 446 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x
460 replacement←' {ψ} X x lt = record { proj1 = {!!} 447 replacement← {ψ} X x lt = record { proj1 = lemma
461 ; proj2 = def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))} 448 ; proj2 = sup-o∋ψx
462 { od→ord (ord→od (od→ord (ψ x)))} (sup-c< ψ {x}) refl (sym diso)
463 } 449 }
464 where 450 where
465 -- (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y → 451 sup-o∋ψx : Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od (od→ord (ψ x))
466 -- ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) 452 sup-o∋ψx = def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))} { od→ord (ord→od (od→ord (ψ x)))}
467 lemma : (y : Ordinal) → ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) → {!!} 453 (sup-c< ψ {x}) refl (sym diso)
468 lemma y not = {!!} 454 lemma : (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y →
469 replacement→' : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y)) 455 ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁)))
470 replacement→' {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where 456 lemma y lt1 not = not (minα (od→ord x) (sup-x ( λ w → od→ord (ψ (ord→od w ))))) (record {
457 proj1 = ?
458 ; proj2 = subst₂ (λ k j → k == j ) refl oiso (o≡→== {!!}) } ) where
459 lemma1 : y o< osuc ( od→ord (ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w ))) ))))
460 lemma1 = o<-subst (sup-lb lt1) diso refl
461 lemma2 : ord→od y ≡ ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w )))))
462 lemma2 with osuc-≡< lemma1
463 lemma2 | case1 refl = subst (λ k → ord→od y ≡ k ) oiso refl
464 lemma2 | case2 t = {!!}
465 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
466 replacement→ {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where
471 lemma : ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) 467 lemma : ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
472 lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 )) 468 lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 ))
473 -- ord→od (od→ord x) == ψ (Ord y)
474 replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x
475 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
476 lemma : def (in-codomain X ψ) (od→ord (ψ x))
477 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym (trans Ord-ord oiso ))} ))
478 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
479 replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) )
480 469
481 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 470 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
482 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 471 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
483 regularity : (x : HOD) (not : ¬ (x == od∅)) → 472 regularity : (x : HOD) (not : ¬ (x == od∅)) →
484 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 473 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)