comparison OD.agda @ 339:feb0fcc430a9

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Jul 2020 19:55:37 +0900
parents bca043423554
children 639fbb6284d8
comparison
equal deleted inserted replaced
338:bca043423554 339:feb0fcc430a9
101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y 102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y
103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal 103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal
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 -- another form of infinite
107 -- pair-ord< : {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x)
108
109 postulate odAxiom : ODAxiom 106 postulate odAxiom : ODAxiom
110 open ODAxiom odAxiom 107 open ODAxiom odAxiom
108
109 -- possible restriction
110 hod-ord< : {x : HOD } → Set n
111 hod-ord< {x} = od→ord x o< next (odmax x)
111 112
112 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD 113 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
113 ¬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) → ⊥
114 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) 115 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
115 116
219 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where 220 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where
220 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) 221 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
221 lemma {t} (case1 refl) = omax-x _ _ 222 lemma {t} (case1 refl) = omax-x _ _
222 lemma {t} (case2 refl) = omax-y _ _ 223 lemma {t} (case2 refl) = omax-y _ _
223 224
225 -- another form of infinite
226 pair-ord< : {x : Ordinal } → Set n
227 pair-ord< {x} = od→ord ( ord→od x , ord→od x ) o< next x
224 228
225 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 229 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
226 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) 230 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
227 231
228 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD 232 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD
368 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax 372 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
369 373
370 infinite : HOD 374 infinite : HOD
371 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 375 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
372 376
373 -- infinite' : HOD 377 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD
374 -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where 378 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where
375 -- u : (y : Ordinal ) → HOD 379 u : (y : Ordinal ) → HOD
376 -- u y = Union (ord→od y , (ord→od y , ord→od y)) 380 u y = Union (ord→od y , (ord→od y , ord→od y))
377 -- lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 381 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
378 -- lemma {o∅} iφ = {!!} 382 lemma {o∅} iφ = proj1 next-limit
379 -- lemma (isuc {y} x) = {!!} where 383 lemma (isuc {y} x) = lemma2 where
380 -- lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y ))) 384 lemma0 : y o< next o∅
381 -- lemma1 = {!!} 385 lemma0 = lemma x
386 lemma3 : odef (u y ) y
387 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
388 lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y
389 lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
390 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
391 lemma1 = ho<
392 lemma2 : od→ord (u y) o< next o∅
393 lemma2 = {!!}
382 394
383 395
384 _=h=_ : (x y : HOD) → Set n 396 _=h=_ : (x y : HOD) → Set n
385 x =h= y = od x == od y 397 x =h= y = od x == od y
386 398