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

comparison OD.agda @ 258:63df67b6281c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 04 Sep 2019 01:12:18 +0900
parents 53b7acd63481
children f714fe999102
comparison
equal deleted inserted replaced
257:53b7acd63481 258:63df67b6281c
55 Ord : ( a : Ordinal ) → OD 55 Ord : ( a : Ordinal ) → OD
56 Ord a = record { def = λ y → y o< a } 56 Ord a = record { def = λ y → y o< a }
57 57
58 od∅ : OD 58 od∅ : OD
59 od∅ = Ord o∅ 59 od∅ = Ord o∅
60
61 -- next assumptions are our axiom
62 -- it defines a subset of OD, which is called HOD, usually defined as
63 -- HOD = { x | TC x ⊆ OD }
64 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
60 65
61 postulate 66 postulate
62 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 67 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
63 od→ord : OD → Ordinal 68 od→ord : OD → Ordinal
64 ord→od : Ordinal → OD 69 ord→od : Ordinal → OD
65 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y 70 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
66 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x 71 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
67 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 72 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
68 -- we should prove this in agda, but simply put here 73 -- we should prove this in agda, but simply put here
69 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 74 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
70 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set 75 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
71 -- 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
72 -- ord→od x ≡ Ord x results the same 77 -- ord→od x ≡ Ord x results the same
73 -- supermum as Replacement Axiom 78 -- supermum as Replacement Axiom
74 sup-o : ( Ordinal → Ordinal ) → Ordinal 79 sup-o : ( Ordinal → Ordinal ) → Ordinal
75 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ 80 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
76 -- contra-position of mimimulity of supermum required in Power Set Axiom 81 -- contra-position of mimimulity of supermum required in Power Set Axiom
77 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal 82 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal
78 -- 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 ψ))
79 -- mimimul and x∋minimul is an Axiom of choice 84 -- mimimul and x∋minimal is an Axiom of choice
80 minimul : (x : OD ) → ¬ (x == od∅ )→ OD 85 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
81 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 86 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
82 x∋minimul : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) 87 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
83 -- minimulity (may proved by ε-induction ) 88 -- minimality (may proved by ε-induction )
84 minimul-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) 89 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
90
91 o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y) x ) → {x : OD } → x ≡ Ord (od→ord x)
92 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
93 lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
94 lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt))
95 lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y
96 lemma2 {y} lt = subst (λ k → def k y ) oiso (o<→c< {y} {od→ord x} lt )
85 97
86 _∋_ : ( a x : OD ) → Set n 98 _∋_ : ( a x : OD ) → Set n
87 _∋_ a x = def a ( od→ord x ) 99 _∋_ a x = def a ( od→ord x )
88 100
89 _c<_ : ( x a : OD ) → Set n 101 _c<_ : ( x a : OD ) → Set n
90 x c< a = a ∋ x 102 x c< a = a ∋ x
91
92 _c≤_ : OD → OD → Set (suc n)
93 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
94 103
95 cseq : {n : Level} → OD → OD 104 cseq : {n : Level} → OD → OD
96 cseq x = record { def = λ y → def x (osuc y) } where 105 cseq x = record { def = λ y → def x (osuc y) } where
97 106
98 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x 107 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x
110 otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y 119 otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y
111 otrans x<a y<x = ordtrans y<x x<a 120 otrans x<a y<x = ordtrans y<x x<a
112 121
113 def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X 122 def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X
114 def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso 123 def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso
124
115 125
116 -- avoiding lv != Zero error 126 -- avoiding lv != Zero error
117 orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y 127 orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y
118 orefl refl = refl 128 orefl refl = refl
119 129
133 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)
134 lemma ox ox refl = eq-refl 144 lemma ox ox refl = eq-refl
135 145
136 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
137 o≡→== {x} {.x} refl = eq-refl 147 o≡→== {x} {.x} refl = eq-refl
138
139 c≤-refl : {n : Level} → ( x : OD ) → x c≤ x
140 c≤-refl x = case1 refl
141 148
142 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ 149 o∅≡od∅ : ord→od (o∅ ) ≡ od∅
143 o∅≡od∅ = ==→o≡ lemma where 150 o∅≡od∅ = ==→o≡ lemma where
144 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x 151 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x
145 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
294 ps = record { def = λ x → p } 301 ps = record { def = λ x → p }
295 lemma : ps == od∅ → p → ⊥ 302 lemma : ps == od∅ → p → ⊥
296 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 ) 303 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
297 ¬p : (od→ord ps ≡ o∅) → p → ⊥ 304 ¬p : (od→ord ps ≡ o∅) → p → ⊥
298 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) 305 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
299 p∨¬p p | no ¬p = case1 (ppp {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where 306 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
300 ps = record { def = λ x → p } 307 ps = record { def = λ x → p }
301 eqo∅ : ps == od∅ → od→ord ps ≡ o∅ 308 eqo∅ : ps == od∅ → od→ord ps ≡ o∅
302 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 309 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
303 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) 310 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
304 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) 311 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
305 312
306 decp : ( p : Set n ) → Dec p -- assuming axiom of choice 313 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
307 decp p with p∨¬p p 314 decp p with p∨¬p p
308 decp p | case1 x = yes x 315 decp p | case1 x = yes x
309 decp p | case2 x = no x 316 decp p | case2 x = no x
429 436
430 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 437 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
431 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx 438 union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
432 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) 439 ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
433 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) 440 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
434 union← X z UX∋z = TransFiniteExists _ lemma UX∋z where 441 union← X z UX∋z = FExists _ lemma UX∋z where
435 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) 442 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
436 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 443 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
437 444
438 ψiso : {ψ : OD → Set n} {x y : OD } → ψ x → x ≡ y → ψ y 445 ψiso : {ψ : OD → Set n} {x y : OD } → ψ x → x ≡ y → ψ y
439 ψiso {ψ} t refl = t 446 ψiso {ψ} t refl = t
460 --- Power Set 467 --- Power Set
461 --- 468 ---
462 --- First consider ordinals in OD 469 --- First consider ordinals in OD
463 --- 470 ---
464 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A 471 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
465 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
466 -- 472 --
467 -- 473 --
468 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) 474 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
469 ∩-≡ {a} {b} inc = record { 475 ∩-≡ {a} {b} inc = record {
470 eq→ = λ {x} x<a → record { proj2 = x<a ; 476 eq→ = λ {x} x<a → record { proj2 = x<a ;
471 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 477 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ;
472 eq← = λ {x} x<a∩b → proj2 x<a∩b } 478 eq← = λ {x} x<a∩b → proj2 x<a∩b }
473 -- 479 --
474 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 480 -- Transitive Set case
475 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 481 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t
482 -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t
483 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
476 -- 484 --
477 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t 485 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
478 ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} 486 ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t}
479 lemma refl (lemma1 lemma-eq )where 487 lemma refl (lemma1 lemma-eq )where
480 lemma-eq : ZFSubset (Ord a) t == t 488 lemma-eq : ZFSubset (Ord a) t == t
487 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 495 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
488 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) 496 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
489 lemma = sup-o< 497 lemma = sup-o<
490 498
491 -- 499 --
492 -- Every set in OD is a subset of Ordinals 500 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
501 -- then replace of all elements of the Power set by A ∩ y
493 -- 502 --
494 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) 503 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
495 504
496 -- we have oly double negation form because of the replacement axiom 505 -- we have oly double negation form because of the replacement axiom
497 -- 506 --
498 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) 507 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
499 power→ A t P∋t {x} t∋x = TransFiniteExists _ lemma5 lemma4 where 508 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
500 a = od→ord A 509 a = od→ord A
501 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) 510 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y)))
502 lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t 511 lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
503 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) 512 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
504 lemma3 y eq not = not (proj1 (eq→ eq t∋x)) 513 lemma3 y eq not = not (proj1 (eq→ eq t∋x))
532 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 541 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
533 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 542 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
534 543
535 -- assuming axiom of choice 544 -- assuming axiom of choice
536 regularity : (x : OD) (not : ¬ (x == od∅)) → 545 regularity : (x : OD) (not : ¬ (x == od∅)) →
537 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 546 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
538 proj1 (regularity x not ) = x∋minimul x not 547 proj1 (regularity x not ) = x∋minimal x not
539 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where 548 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
540 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ 549 lemma1 : {x₁ : Ordinal} → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
541 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where 550 lemma1 {x₁} s = ⊥-elim ( minimal-1 x not (ord→od x₁) lemma3 ) where
542 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) 551 lemma3 : def (minimal x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
543 lemma3 = record { proj1 = def-subst {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso) 552 lemma3 = record { proj1 = def-subst {_} {_} {minimal x not} {_} (proj1 s) refl (sym diso)
544 ; proj2 = proj2 (proj2 s) } 553 ; proj2 = proj2 (proj2 s) }
545 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ 554 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁
546 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) 555 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
547 556
548 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 557 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
549 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 558 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
550 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 559 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
567 infinity x lt = def-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where 576 infinity x lt = def-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
568 lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) 577 lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
569 ≡ od→ord (Union (x , (x , x))) 578 ≡ od→ord (Union (x , (x , x)))
570 lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 579 lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso
571 580
572 -- Axiom of choice ( is equivalent to the existence of minimul in our case ) 581 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
573 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 582 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
574 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD 583 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
575 choice-func X {x} not X∋x = minimul x not 584 choice-func X {x} not X∋x = minimal x not
576 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 585 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
577 choice X {A} X∋A not = x∋minimul A not 586 choice X {A} X∋A not = x∋minimal A not
578 587
579 --- 588 ---
580 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice 589 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
581 --- 590 ---
582 record choiced ( X : OD) : Set (suc n) where 591 record choiced ( X : OD) : Set (suc n) where