comparison ODC.agda @ 279:197e0b3d39dc

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 16:41:40 +0900
parents d9d3654baee1
children 5544f4921a44
comparison
equal deleted inserted replaced
278:bfb5e807718b 279:197e0b3d39dc
92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD 92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
93 choice-func X {x} not X∋x = minimal x not 93 choice-func X {x} not X∋x = minimal x not
94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
95 choice X {A} X∋A not = x∋minimal A not 95 choice X {A} X∋A not = x∋minimal A not
96 96
97 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
98 ---
99 record choiced ( X : OD) : Set (suc n) where
100 field
101 a-choice : OD
102 is-in : X ∋ a-choice
103
104 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
105 choice-func' X p∨¬p not = have_to_find where
106 ψ : ( ox : Ordinal ) → Set (suc n)
107 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
108 lemma-ord : ( ox : Ordinal ) → ψ ox
109 lemma-ord ox = TransFinite {ψ} induction ox where
110 ∋-p : (A x : OD ) → Dec ( A ∋ x )
111 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
112 ∋-p A x | case1 (lift t) = yes t
113 ∋-p A x | case2 t = no (λ x → t (lift x ))
114 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
115 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
116 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
117 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
118 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
119 lemma : ¬ ((x : Ordinal ) → A x) → B
120 lemma not with p∨¬p B
121 lemma not | case1 b = b
122 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
123 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
124 induction x prev with ∋-p X ( ord→od x)
125 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
126 ... | no ¬p = lemma where
127 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
128 lemma1 y with ∋-p X (ord→od y)
129 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
130 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
131 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
132 lemma = ∀-imply-or lemma1
133 have_to_find : choiced X
134 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
135 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
136 ¬¬X∋x nn = not record {
137 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
138 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
139 }
140