Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 271:2169d948159b
fix incl
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 30 Dec 2019 23:45:59 +0900 |
parents | 53744836020b |
children | 985a1af11bce |
comparison
equal
deleted
inserted
replaced
270:fc3d4bc1dc5e | 271:2169d948159b |
---|---|
34 eq← : ∀ { x : Ordinal } → def b x → def a x | 34 eq← : ∀ { x : Ordinal } → def b x → def a x |
35 | 35 |
36 id : {A : Set n} → A → A | 36 id : {A : Set n} → A → A |
37 id x = x | 37 id x = x |
38 | 38 |
39 eq-refl : { x : OD } → x == x | 39 ==-refl : { x : OD } → x == x |
40 eq-refl {x} = record { eq→ = id ; eq← = id } | 40 ==-refl {x} = record { eq→ = id ; eq← = id } |
41 | 41 |
42 open _==_ | 42 open _==_ |
43 | 43 |
44 eq-sym : { x y : OD } → x == y → y == x | 44 ==-trans : { x y z : OD } → x == y → y == z → x == z |
45 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } | 45 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } |
46 | 46 |
47 eq-trans : { x y z : OD } → x == y → y == z → x == z | 47 ==-sym : { x y : OD } → x == y → y == x |
48 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } | 48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } |
49 | |
49 | 50 |
50 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y | 51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y |
51 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m | 52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m |
52 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m | 53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m |
53 | 54 |
72 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 73 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
73 ==→o≡ : { x y : OD } → (x == y) → x ≡ y | 74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y |
74 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD | 75 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD |
75 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x | 76 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x |
76 -- ord→od x ≡ Ord x results the same | 77 -- ord→od x ≡ Ord x results the same |
77 -- supermum as Replacement Axiom | 78 -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound ) |
78 sup-o : ( Ordinal → Ordinal ) → Ordinal | 79 sup-o : ( Ordinal → Ordinal ) → Ordinal |
79 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ | 80 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ |
80 -- contra-position of mimimulity of supermum required in Power Set Axiom | 81 -- contra-position of mimimulity of supermum required in Power Set Axiom |
81 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal | 82 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal |
82 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) | 83 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) |
138 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) | 139 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) |
139 | 140 |
140 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y | 141 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y |
141 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where | 142 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where |
142 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy) | 143 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy) |
143 lemma ox ox refl = eq-refl | 144 lemma ox ox refl = ==-refl |
144 | 145 |
145 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y | 146 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y |
146 o≡→== {x} {.x} refl = eq-refl | 147 o≡→== {x} {.x} refl = ==-refl |
147 | 148 |
148 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ | 149 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ |
149 o∅≡od∅ = ==→o≡ lemma where | 150 o∅≡od∅ = ==→o≡ lemma where |
150 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x | 151 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x |
151 lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso | 152 lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso |
160 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ | 161 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ |
161 eq→ ∅0 {w} (lift ()) | 162 eq→ ∅0 {w} (lift ()) |
162 eq← ∅0 {w} lt = lift (¬x<0 lt) | 163 eq← ∅0 {w} lt = lift (¬x<0 lt) |
163 | 164 |
164 ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ ) | 165 ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ ) |
165 ∅< {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d | 166 ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d |
166 ∅< {x} {y} d eq | lift () | 167 ∅< {x} {y} d eq | lift () |
167 | 168 |
168 ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox | 169 ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox |
169 ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x ) | 170 ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x ) |
170 | 171 |
188 left (case1 t) = case2 t | 189 left (case1 t) = case2 t |
189 left (case2 t) = case1 t | 190 left (case2 t) = case1 t |
190 right : {z : Ordinal} → def (y , x) z → def (x , y) z | 191 right : {z : Ordinal} → def (y , x) z → def (x , y) z |
191 right (case1 t) = case2 t | 192 right (case1 t) = case2 t |
192 right (case2 t) = case1 t | 193 right (case2 t) = case1 t |
193 | |
194 ==-trans : { x y z : OD } → x == y → y == z → x == z | |
195 ==-trans x=y y=z = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← = λ {m} t → eq← x=y (eq← y=z t) } | |
196 | |
197 ==-sym : { x y : OD } → x == y → y == x | |
198 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } | |
199 | 194 |
200 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y | 195 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y |
201 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) | 196 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) |
202 | 197 |
203 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y | 198 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y |
337 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set | 332 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set |
338 | 333 |
339 Def : (A : OD ) → OD | 334 Def : (A : OD ) → OD |
340 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | 335 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) |
341 | 336 |
342 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n | 337 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n |
343 _⊆_ A B {x} = A ∋ x → B ∋ x | 338 -- _⊆_ A B {x} = A ∋ x → B ∋ x |
339 | |
340 record _⊆_ ( A B : OD ) : Set (suc n) where | |
341 field | |
342 incl : { x : OD } → A ∋ x → B ∋ x | |
343 | |
344 open _⊆_ | |
344 | 345 |
345 infixr 220 _⊆_ | 346 infixr 220 _⊆_ |
346 | 347 |
347 subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) | 348 subset-lemma : {A x : OD } → ( {y : OD } → x ∋ y → ZFSubset A x ∋ y ) ⇔ ( x ⊆ A ) |
348 subset-lemma {A} {x} {y} = record { | 349 subset-lemma {A} {x} = record { |
349 proj1 = λ z lt → proj1 (z lt) | 350 proj1 = λ lt → record { incl = λ x∋z → proj1 (lt x∋z) } |
350 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } | 351 ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } |
351 } | 352 } |
352 | 353 |
353 open import Data.Unit | 354 open import Data.Unit |
354 | 355 |
355 ε-induction : { ψ : OD → Set (suc n)} | 356 ε-induction : { ψ : OD → Set (suc n)} |
404 | 405 |
405 infixr 200 _∈_ | 406 infixr 200 _∈_ |
406 -- infixr 230 _∩_ _∪_ | 407 -- infixr 230 _∩_ _∪_ |
407 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite | 408 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite |
408 isZF = record { | 409 isZF = record { |
409 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } | 410 isEquivalence = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans } |
410 ; pair→ = pair→ | 411 ; pair→ = pair→ |
411 ; pair← = pair← | 412 ; pair← = pair← |
412 ; union→ = union→ | 413 ; union→ = union→ |
413 ; union← = union← | 414 ; union← = union← |
414 ; empty = empty | 415 ; empty = empty |
434 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) | 435 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) |
435 | 436 |
436 empty : (x : OD ) → ¬ (od∅ ∋ x) | 437 empty : (x : OD ) → ¬ (od∅ ∋ x) |
437 empty x = ¬x<0 | 438 empty x = ¬x<0 |
438 | 439 |
439 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z} | 440 o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) |
440 o<→c< lt lt1 = ordtrans lt1 lt | 441 o<→c< lt = record { incl = λ z → ordtrans z lt } |
441 | 442 |
442 ⊆→o< : {x y : Ordinal } → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y | 443 ⊆→o< : {x y : Ordinal } → (Ord x) ⊆ (Ord y) → x o< osuc y |
443 ⊆→o< {x} {y} lt with trio< x y | 444 ⊆→o< {x} {y} lt with trio< x y |
444 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc | 445 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc |
445 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc | 446 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc |
446 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) | 447 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) |
447 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) | 448 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) |
448 | 449 |
449 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z | 450 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z |
450 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx | 451 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx |
451 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) | 452 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) |
549 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 550 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
550 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 551 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |
551 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) | 552 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) |
552 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) | 553 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) |
553 | 554 |
554 ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x} | 555 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) |
555 ord⊆power a x lt = power← (Ord a) x lemma where | 556 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where |
556 lemma : {y : OD} → x ∋ y → Ord a ∋ y | 557 lemma : {x y : OD} → od→ord x o< osuc a → x ∋ y → Ord a ∋ y |
557 lemma y<x with osuc-≡< lt | 558 lemma lt y<x with osuc-≡< lt |
558 lemma y<x | case1 refl = c<→o< y<x | 559 lemma lt y<x | case1 refl = c<→o< y<x |
559 lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a | 560 lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a |
560 | 561 |
561 -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | 562 -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a) |
562 -- continuum-hyphotheis a x = ? | 563 -- continuum-hyphotheis a = ? |
563 | 564 |
564 -- assuming axiom of choice | 565 -- assuming axiom of choice |
565 regularity : (x : OD) (not : ¬ (x == od∅)) → | 566 regularity : (x : OD) (not : ¬ (x == od∅)) → |
566 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) | 567 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
567 proj1 (regularity x not ) = x∋minimal x not | 568 proj1 (regularity x not ) = x∋minimal x not |
618 ψ : ( ox : Ordinal ) → Set (suc n) | 619 ψ : ( ox : Ordinal ) → Set (suc n) |
619 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X | 620 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X |
620 lemma-ord : ( ox : Ordinal ) → ψ ox | 621 lemma-ord : ( ox : Ordinal ) → ψ ox |
621 lemma-ord ox = TransFinite {ψ} induction ox where | 622 lemma-ord ox = TransFinite {ψ} induction ox where |
622 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 623 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
623 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) | 624 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM |
624 ∋-p A x | case1 (lift t) = yes t | 625 ∋-p A x | case1 (lift t) = yes t |
625 ∋-p A x | case2 t = no (λ x → t (lift x )) | 626 ∋-p A x | case2 t = no (λ x → t (lift x )) |
626 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } | 627 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } |
627 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B | 628 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B |
628 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) | 629 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM |
629 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t | 630 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t |
630 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where | 631 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where |
631 lemma : ¬ ((x : Ordinal ) → A x) → B | 632 lemma : ¬ ((x : Ordinal ) → A x) → B |
632 lemma not with p∨¬p B | 633 lemma not with p∨¬p B |
633 lemma not | case1 b = b | 634 lemma not | case1 b = b |
641 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) | 642 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) |
642 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) | 643 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) |
643 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X | 644 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X |
644 lemma = ∀-imply-or lemma1 | 645 lemma = ∀-imply-or lemma1 |
645 have_to_find : choiced X | 646 have_to_find : choiced X |
646 have_to_find with lemma-ord (od→ord X ) | 647 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where |
647 have_to_find | t = dont-or t ¬¬X∋x where | |
648 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) | 648 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) |
649 ¬¬X∋x nn = not record { | 649 ¬¬X∋x nn = not record { |
650 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | 650 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) |
651 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | 651 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) |
652 } | 652 } |