comparison OD.agda @ 298:3795ffb127d0

... should we use HOD?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jun 2020 11:14:30 +0900
parents be6670af87fa
children 171f23379e2e
comparison
equal deleted inserted replaced
297:be6670af87fa 298:3795ffb127d0
71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
72 field 72 field
73 maxod : Ordinal 73 maxod : Ordinal
74 od→ord : OD → Ordinal 74 od→ord : OD → Ordinal
75 ord→od : (x : Ordinal ) → x o< maxod → OD 75 ord→od : (x : Ordinal ) → x o< maxod → OD
76 -- ZFSet has bounded solution of OD
76 o<max : {x : OD } → od→ord x o< maxod 77 o<max : {x : OD } → od→ord x o< maxod
78 def<maxod : {x y : Ordinal} → (lt : x o< maxod) → def (ord→od x lt ) y → y o< maxod
77 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y 79 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
78 oiso : {x : OD } → ord→od ( od→ord x ) o<max ≡ x 80 oiso : {x : OD } → ord→od ( od→ord x ) o<max ≡ x
79 diso : {x : Ordinal } → (lt : x o< maxod) → od→ord ( ord→od x lt ) ≡ x 81 diso : {x : Ordinal } → (lt : x o< maxod) → od→ord ( ord→od x lt ) ≡ x
80 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 82 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
81 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) 83 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
105 107
106 od∅ : OD 108 od∅ : OD
107 od∅ = Ord o∅ 109 od∅ = Ord o∅
108 110
109 111
112 -- = subst (λ k → k o< maxod ) (diso {!!}) ( ordtrans ( c<→o< lt ) o<max )
110 -- o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y {!!} ) x ) → {x : OD } → x ≡ Ord (od→ord x) 113 -- o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y {!!} ) x ) → {x : OD } → x ≡ Ord (od→ord x)
111 -- o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where 114 -- o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
112 -- lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y 115 -- lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
113 -- 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)) 116 -- 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))
114 -- lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y 117 -- lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y
140 143
141 -- def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X 144 -- def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X
142 -- def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym (diso lemma)))) (diso lemma) (diso o<max) where 145 -- def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym (diso lemma)))) (diso lemma) (diso o<max) where
143 -- lemma : x o< maxod 146 -- lemma : x o< maxod
144 -- lemma = subst (λ k → k o< maxod ) (diso {!!} ) (otrans o<max ( c<→o< lt )) 147 -- lemma = subst (λ k → k o< maxod ) (diso {!!} ) (otrans o<max ( c<→o< lt ))
145
146
147 -- avoiding lv != Zero error
148 orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y
149 orefl refl = refl
150 148
151 ==-iso : { x y : OD } → ord→od (od→ord x) o<max == ord→od (od→ord y) o<max → x == y 149 ==-iso : { x y : OD } → ord→od (od→ord x) o<max == ord→od (od→ord y) o<max → x == y
152 ==-iso {x} {y} eq = record { 150 ==-iso {x} {y} eq = record {
153 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ; 151 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ;
154 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) } 152 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) }
157 lemma {x} {z} d = def-subst d oiso refl 155 lemma {x} {z} d = def-subst d oiso refl
158 156
159 =-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) o<max == y) 157 =-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) o<max == y)
160 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) 158 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso)
161 159
160 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
161 --
162 <-irr : {x y z : Ordinal } → x ≡ y → (x o< z) ≡ (y o< z) 162 <-irr : {x y z : Ordinal } → x ≡ y → (x o< z) ≡ (y o< z)
163 <-irr refl = refl 163 <-irr refl = refl
164 164
165 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y 165 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y
166 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq) o<max o<max ) where 166 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) eq o<max o<max ) where
167 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (x<m : ox o< maxod) (y<m : oy o< maxod) → (ord→od ox x<m ) == (ord→od oy y<m ) 167 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (x<m : ox o< maxod) (y<m : oy o< maxod) → (ord→od ox x<m ) == (ord→od oy y<m )
168 lemma ox ox refl x<m y<m = subst (λ k → ord→od ox x<m == ord→od ox k) {!!} ==-refl 168 lemma ox ox refl x<m y<m = subst (λ k → ord→od ox x<m == ord→od ox k) {!!} ==-refl
169 169
170 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x {!!} == ord→od y {!!} 170 o≡→== : { x y : Ordinal } → x ≡ y → (lx : x o< maxod ) → (ly : y o< maxod ) → ord→od x lx == ord→od y ly
171 o≡→== {x} {.x} refl = ==-refl 171 o≡→== {x} {.x} refl _ _ = {!!} -- ==-refl
172 172
173 o∅≡od∅ : ord→od (o∅ ) {!!} ≡ od∅ 173 o∅<maxod : o∅ o< maxod
174 o∅<maxod with IsOrdinals.OTri (Ordinals.isOrdinal O) o∅ maxod
175 o∅<maxod | tri< a ¬b ¬c = a
176 o∅<maxod | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 (subst (λ k → (od→ord record { def = λ x → One }) o< k ) (sym b) o<max ))
177 o∅<maxod | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
178
179 o∅≡od∅ : ord→od o∅ o∅<maxod ≡ od∅
174 o∅≡od∅ = ==→o≡ lemma where 180 o∅≡od∅ = ==→o≡ lemma where
175 lemma0 : {x : Ordinal} → def (ord→od o∅ {!!} ) x → def od∅ x 181 lemma0 : {x : Ordinal} → x o< maxod → def (ord→od o∅ o∅<maxod) x → def od∅ x
176 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 {!!}) 182 lemma0 {x} x<m lt = o<-subst (c<→o< {ord→od x x<m } {ord→od o∅ o∅<maxod}
177 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅ {!!} ) x 183 (def-subst {ord→od o∅ o∅<maxod} {x} lt refl (sym (diso x<m ))) ) (diso x<m) (diso o∅<maxod)
184 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅ o∅<maxod ) x
178 lemma1 {x} lt = ⊥-elim (¬x<0 lt) 185 lemma1 {x} lt = ⊥-elim (¬x<0 lt)
179 lemma : ord→od o∅ {!!} == od∅ 186 lemma : ord→od o∅ o∅<maxod == od∅
180 lemma = record { eq→ = lemma0 ; eq← = lemma1 } 187 lemma = record { eq→ = λ {x} lt → lemma0 (def<maxod o∅<maxod lt ) lt ; eq← = lemma1 }
181 188
182 ord-od∅ : od→ord (od∅ ) ≡ o∅ 189 ord-od∅ : od→ord (od∅ ) ≡ o∅
183 ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) (diso {!!}) (cong ( λ k → od→ord k ) o∅≡od∅ ) ) 190 ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) (diso o∅<maxod) (cong ( λ k → od→ord k ) o∅≡od∅ ) )
184 191
185 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ 192 ∅0 : record { def = λ x → Lift n ⊥ } == od∅
186 eq→ ∅0 {w} (lift ()) 193 eq→ ∅0 {w} (lift ())
187 eq← ∅0 {w} lt = lift (¬x<0 lt) 194 eq← ∅0 {w} lt = lift (¬x<0 lt)
188 195
206 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) 213 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y))
207 214
208 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 215 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
209 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 216 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
210 217
218
211 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD 219 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
212 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y {!!} ))))) } 220 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (lt : def X y ) → (lt : y o< maxod) → ( x ≡ od→ord (ψ (ord→od y lt ))))) } where
213 221
214 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 222 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
215 223
216 ZFSubset : (A x : OD ) → OD 224 ZFSubset : (A x : OD ) → OD
217 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set 225 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
310 -- ; choice-func = choice-func 318 -- ; choice-func = choice-func
311 -- ; choice = choice 319 -- ; choice = choice
312 } where 320 } where
313 321
314 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) 322 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
315 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) 323 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x {!!} {!!} ))
316 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) 324 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y {!!} {!!} ))
317 325
318 pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t 326 pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t
319 pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) 327 pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
320 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) 328 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
321 329
348 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 356 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
349 } 357 }
350 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 358 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
351 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where 359 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where
352 lemma : def (in-codomain X ψ) (od→ord (ψ x)) 360 lemma : def (in-codomain X ψ) (od→ord (ψ x))
353 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) 361 lemma not = ⊥-elim ( not ( od→ord x ) {!!} ) -- (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
354 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) 362 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
355 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where 363 replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
356 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} )))) 364 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} ))))
357 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))) 365 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )))
358 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where 366 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
359 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) 367 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))
360 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq ) 368 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq {!!} {!!} )
361 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) ) 369 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) )
362 lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso ( proj2 not2 )) 370 lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso ( proj2 not2 ))
363 371
364 --- 372 ---
365 --- Power Set 373 --- Power Set
431 439
432 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) 440 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x))
433 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) 441 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x)))
434 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) 442 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} )
435 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 443 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
436 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 444 lemma2 not = ⊥-elim ( not (od→ord t) {!!}) where -- (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
437 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t) {!!} ) 445 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t) {!!} )
438 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 446 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
439 447
440 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 448 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
441 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where 449 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where