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

comparison HOD.agda @ 148:6e767ad3edc2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
give up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 19:45:59 +0900
parents c848550c8b39
children ebcbfd9d9c8e
comparison
equal deleted inserted replaced
147:c848550c8b39 148:6e767ad3edc2
161 ∋→o< : {n : Level} → { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a 161 ∋→o< : {n : Level} → { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
162 ∋→o< {n} {a} {x} lt = t where 162 ∋→o< {n} {a} {x} lt = t where
163 t : (od→ord x) o< (od→ord a) 163 t : (od→ord x) o< (od→ord a)
164 t = c<→o< {suc n} {x} {a} lt 164 t = c<→o< {suc n} {x} {a} lt
165 165
166 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 166 -- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
167 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
168 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
169 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
170 lemma lt = {!!}
171 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
172 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
173 167
174 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) 168 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x )
175 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where 169 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
176 170
177 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y 171 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y
199 193
200 194
201 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 195 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
202 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) 196 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
203 197
204 csuc : {n : Level} → OD {suc n} → OD {suc n}
205 csuc x = Ord ( osuc ( od→ord x ))
206
207 in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n} 198 in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n}
208 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (Ord y ))))) } 199 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
209 200
210 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 201 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
211 202
212 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} 203 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
213 ZFSubset A x = record { def = λ y → def A y ∧ def x y } where 204 ZFSubset A x = record { def = λ y → def A y ∧ def x y } where
340 } 331 }
341 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 332 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
342 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where 333 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
343 lemma : def (in-codomain X ψ) (od→ord (ψ x)) 334 lemma : def (in-codomain X ψ) (od→ord (ψ x))
344 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) 335 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
345 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso {!!} )) } )) 336 {!!} } ))
346 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) 337 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
347 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 338 replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
348 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y)))) 339 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
349 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y))) 340 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
350 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where 341 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
351 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y)) 342 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))
352 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq ) 343 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) == k ) oiso (o≡→== eq )
449 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} 440 lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
450 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where 441 ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
451 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t)) 442 lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t))
452 lemma5 = cong (λ k → od→ord (A ∩ k )) {!!} 443 lemma5 = cong (λ k → od→ord (A ∩ k )) {!!}
453 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 444 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
454 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where 445 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = {!!} }) ) where
455 446
456 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 447 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
457 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 448 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
458 regularity : (x : OD) (not : ¬ (x == od∅)) → 449 regularity : (x : OD) (not : ¬ (x == od∅)) →
459 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 450 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)