Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 138:567084f2278f
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Jul 2019 17:37:26 +0900 |
parents | c7c9f3efc428 |
children | 53077af367e9 |
line wrap: on
line diff
--- a/HOD.agda Sun Jul 07 08:56:25 2019 +0900 +++ b/HOD.agda Sun Jul 07 17:37:26 2019 +0900 @@ -446,19 +446,37 @@ lemma : X ∋ union-u {X} {z} X∋z lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord - ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y - ψiso {ψ} t refl = t + -- ψiso : {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y → ψ y + -- ψiso {ψ} t refl = t selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y) selection {X} {ψ} {y} = record { proj1 = λ s → record { proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) } - ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso ))) + ; proj2 = λ s → record { proj1 = λ y1 dy1 → + subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso ))) ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where + -- ψ< : {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} → ψ y ∋ x → ψ y' == x + -- ψ< = {!!} + replacement←' : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace' X ψ ∋ ψ x + replacement←' {ψ} X x lt = record { proj1 = {!!} + ; proj2 = def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))} + { od→ord (ord→od (od→ord (ψ x)))} (sup-c< ψ {x}) refl (sym diso) + } + where + -- (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y → + -- ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) + lemma : (y : Ordinal) → ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) → {!!} + lemma y not = {!!} + replacement→' : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y)) + replacement→' {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where + lemma : ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) ) + lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 )) + -- ord→od (od→ord x) == ψ (Ord y) replacement← : {ψ : HOD → HOD} (X x : HOD) → X ∋ x → Replace X ψ ∋ ψ x replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where lemma : def (in-codomain X ψ) (od→ord (ψ x)) lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym (trans Ord-ord oiso ))} )) - replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (ψ x == y)) - replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) ) + replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y)) + replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) ) ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq