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

comparison OD.agda @ 344:e0916a632971

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
possible order restriction makes ω ZFSet
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Jul 2020 14:45:57 +0900
parents 34e71402d579
children 06f10815d0b3
comparison
equal deleted inserted replaced
343:34e71402d579 344:e0916a632971
104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ 104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ
105 105
106 postulate odAxiom : ODAxiom 106 postulate odAxiom : ODAxiom
107 open ODAxiom odAxiom 107 open ODAxiom odAxiom
108 108
109 -- possible restriction 109 -- possible order restriction
110 hod-ord< : {x : HOD } → Set n 110 hod-ord< : {x : HOD } → Set n
111 hod-ord< {x} = od→ord x o< next (odmax x) 111 hod-ord< {x} = od→ord x o< next (odmax x)
112 112
113 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD 113 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
114 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ 114 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
235 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x) 235 lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
236 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡) 236 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
237 lemmab1 : od→ord (x , x) o< next ( odmax (x , x)) 237 lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
238 lemmab1 = ho< 238 lemmab1 = ho<
239 239
240 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
241 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
242
243 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
244 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
245
246 ZFSubset : (A x : HOD ) → HOD
247 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
248 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
249 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
250
251 record _⊆_ ( A B : HOD ) : Set (suc n) where
252 field
253 incl : { x : HOD } → A ∋ x → B ∋ x
254
255 open _⊆_
256 infixr 220 _⊆_
257
258 od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
259 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
260
261 -- if we have od→ord (x , x) ≡ osuc (od→ord x), ⊆→o≤ → c<→o<
262 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y) 240 pair<y : {x y : HOD } → y ∋ x → od→ord (x , x) o< osuc (od→ord y)
263 pair<y {x} {y} y∋x = ⊆→o≤ lemma where 241 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
264 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z 242 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
265 lemma (case1 refl) = y∋x 243 lemma (case1 refl) = y∋x
266 lemma (case2 refl) = y∋x 244 lemma (case2 refl) = y∋x
267 245
246 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
247 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
248
249 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
250 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
251
252 ZFSubset : (A x : HOD ) → HOD
253 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
254 lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
255 lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
256
257 record _⊆_ ( A B : HOD ) : Set (suc n) where
258 field
259 incl : { x : HOD } → A ∋ x → B ∋ x
260
261 open _⊆_
262 infixr 220 _⊆_
263
264 od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
265 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
266
267 -- if we have od→ord (x , x) ≡ osuc (od→ord x), ⊆→o≤ → c<→o<
268 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) ) 268 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
269 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) ) 269 → ({y z : HOD } → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
270 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y 270 → {x y : HOD } → def (od y) ( od→ord x ) → od→ord x o< od→ord y
271 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y) 271 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y)
272 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a 272 ⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
392 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 392 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
393 lemma {o∅} iφ = proj1 next-limit 393 lemma {o∅} iφ = proj1 next-limit
394 lemma (isuc {y} x) = lemma2 where 394 lemma (isuc {y} x) = lemma2 where
395 lemma0 : y o< next o∅ 395 lemma0 : y o< next o∅
396 lemma0 = lemma x 396 lemma0 = lemma x
397 lemma3 : odef (u y ) y
398 lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
399 lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y
400 lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
401 lemma5 : y o< odmax (u y)
402 lemma5 = <odmax (u y) lemma3
403 lemma6 : y o< odmax (ord→od y , (ord→od y , ord→od y))
404 lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl))
405 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y)) 397 lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
406 lemma8 = ho< 398 lemma8 = ho<
407 --- (x,y) < next (omax x y) < next (osuc y) = next y 399 --- (x,y) < next (omax x y) < next (osuc y) = next y
408 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y) 400 lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
409 lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< ) 401 lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
410 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y)) 402 lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
411 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8) 403 lemma81 = nexto=n (subst (λ k → od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
412 lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
413 lemma91 = c<→o< (case1 refl)
414 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y)) 404 lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
415 lemma9 = lemmaa (c<→o< (case1 refl)) 405 lemma9 = lemmaa (c<→o< (case1 refl))
416 lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y)) 406 lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
417 lemma71 = next< lemma81 lemma9 407 lemma71 = next< lemma81 lemma9
418 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) 408 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))