Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal-definable.agda @ 104:d92411bed18c
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 16 Jun 2019 02:06:09 +0900 |
parents | c8b79d303867 |
children | ec6235ce0215 |
comparison
equal
deleted
inserted
replaced
103:c8b79d303867 | 104:d92411bed18c |
---|---|
55 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} | 55 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} |
56 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ | 56 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ |
57 -- a contra-position of minimality of supermum | 57 -- a contra-position of minimality of supermum |
58 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} | 58 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} |
59 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) | 59 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) |
60 -- sup-min : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → {z : Ordinal {n}} → ψ z o< z → sup-o ψ o< osuc z | |
61 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} | |
62 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) | |
63 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) | |
64 | |
60 | 65 |
61 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n | 66 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n |
62 _∋_ {n} a x = def a ( od→ord x ) | 67 _∋_ {n} a x = def a ( od→ord x ) |
63 | 68 |
64 _c<_ : { n : Level } → ( x a : OD {n} ) → Set n | 69 Ord : { n : Level } → ( a : Ordinal {suc n} ) → OD {suc n} |
65 x c< a = od→ord x o< od→ord a | 70 Ord {n} a = record { def = λ y → y o< a } |
66 | 71 |
67 postulate | 72 _c<_ : { n : Level } → ( x a : Ordinal {n} ) → Set n |
68 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y | 73 x c< a = Ord a ∋ Ord x |
74 | |
75 c<→o< : { n : Level } → { x a : OD {n} } → record { def = λ y → y o< od→ord a } ∋ x → od→ord x o< od→ord a | |
76 c<→o< lt = lt | |
77 | |
78 o<→c< : { n : Level } → { x a : OD {n} } → od→ord x o< od→ord a → record { def = λ y → y o< od→ord a } ∋ x | |
79 o<→c< lt = lt | |
80 | |
81 ==→o≡' : {n : Level} → { x y : Ordinal {suc n} } → Ord x == Ord y → x ≡ y | |
82 ==→o≡' {n} {x} {y} eq with trio< {n} x y | |
83 ==→o≡' {n} {x} {y} eq | tri< a ¬b ¬c with eq← eq {x} a | |
84 ... | t = ⊥-elim ( o<¬≡ x x refl t ) | |
85 ==→o≡' {n} {x} {y} eq | tri≈ ¬a refl ¬c = refl | |
86 ==→o≡' {n} {x} {y} eq | tri> ¬a ¬b c with eq→ eq {y} c | |
87 ... | t = ⊥-elim ( o<¬≡ y y refl t ) | |
88 | |
89 ∅∨ : { n : Level } → { x y : Ordinal {suc n} } → ( Ord {n} x == Ord y ) ∨ ( ¬ ( Ord x == Ord y ) ) | |
90 ∅∨ {n} {x} {y} with trio< x y | |
91 ∅∨ {n} {x} {y} | tri< a ¬b ¬c = case2 ( λ eq → ¬b ( ==→o≡' eq ) ) | |
92 ∅∨ {n} {x} {y} | tri≈ ¬a refl ¬c = case1 ( record { eq→ = id ; eq← = id } ) | |
93 ∅∨ {n} {x} {y} | tri> ¬a ¬b c = case2 ( λ eq → ¬b ( ==→o≡' eq ) ) | |
94 | |
95 ¬x∋x' : { n : Level } → { x : Ordinal {n} } → ¬ ( record { def = λ y → y o< x } ∋ record { def = λ y → y o< x } ) | |
96 ¬x∋x' {n} {record { lv = Zero ; ord = ord }} (case1 ()) | |
97 ¬x∋x' {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = lx ; ord = Φ lx }} (case1 {!!}) | |
98 ¬x∋x' {n} {record { lv = Suc lx ; ord = OSuc (Suc lx) ox }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = Suc lx ; ord = ox}} (case1 {!!}) | |
99 ¬x∋x' {n} {record { lv = lv ; ord = Φ (lv) }} (case2 ()) | |
100 ¬x∋x' {n} {record { lv = lv ; ord = OSuc (lv) ox }} (case2 x) = | |
101 ¬x∋x' {n} {record { lv = lv ; ord = ox }} (case2 {!!}) | |
102 | |
103 ¬x∋x : { n : Level } → { x : OD {n} } → ¬ x ∋ x | |
104 ¬x∋x = {!!} | |
105 | |
106 oc-lemma : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → def (record { def = λ y → y o< oa }) oa → ⊥ | |
107 oc-lemma {n} {x} {oa} lt = o<¬≡ oa oa refl lt | |
108 | |
109 oc-lemma1 : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → od→ord (record { def = λ y → y o< oa }) o< oa → ⊥ | |
110 oc-lemma1 {n} {x} {oa} lt = ¬x∋x' {n} lt -- lt : def (record { def = λ y → y o< oa }) (record { def = λ y → y o< oa }) | |
111 | |
112 oc-lemma2 : { n : Level } → { x a : OD {n} } → { oa : Ordinal {n} } → oa o< od→ord (record { def = λ y → y o< oa }) → ⊥ | |
113 oc-lemma2 {n} {x} {oa} lt = {!!} | |
69 | 114 |
70 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) | 115 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) |
71 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) | 116 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) |
72 | 117 |
73 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x | 118 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x |
74 def-subst df refl refl = df | 119 def-subst df refl refl = df |
75 | 120 |
76 -- sup-min : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → {z : Ordinal {n}} → ψ z o< z → sup-o ψ o< osuc z | 121 o<-def : {n : Level } {x y : Ordinal {n} } → x o< y → def (record { def = λ x → x o< y }) x |
122 o<-def x<y = x<y | |
123 | |
124 def-o< : {n : Level } {x y : Ordinal {n} } → def (record { def = λ x → x o< y }) x → x o< y | |
125 def-o< x<y = x<y | |
77 | 126 |
78 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} | 127 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} |
79 sup-od ψ = ord→od ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) | 128 sup-od ψ = ord→od ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) |
80 | 129 |
81 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x )) | 130 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x )) |
82 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )} | 131 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )} |
83 {!!} refl (cong ( λ k → od→ord (ψ k) ) oiso) | 132 {!!} refl (cong ( λ k → od→ord (ψ k) ) oiso) |
84 | 133 |
85 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) | 134 od∅' : {n : Level} → OD {n} |
86 ∅1 {n} x = {!!} | 135 od∅' = record { def = λ x → x o< o∅ } |
136 | |
137 ∅0 : {n : Level} → od∅ {suc n} == record { def = λ x → x o< o∅ } | |
138 eq→ ∅0 {w} (lift ()) | |
139 eq← ∅0 {w} (case1 ()) | |
140 eq← ∅0 {w} (case2 ()) | |
141 | |
142 ∅1 : {n : Level} → ( x : Ordinal {n} ) → ¬ ( x c< o∅ {n} ) | |
143 ∅1 {n} x lt = {!!} | |
87 | 144 |
88 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} | 145 ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} |
89 ∅3 {n} {x} = TransFinite {n} c2 c3 x where | 146 ∅3 {n} {x} = TransFinite {n} c2 c3 x where |
90 c0 : Nat → Ordinal {n} → Set n | 147 c0 : Nat → Ordinal {n} → Set n |
91 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} | 148 c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} |
100 c3 lx (Φ .lx) d not | t | () | 157 c3 lx (Φ .lx) d not | t | () |
101 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) | 158 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) |
102 ... | t with t (case2 (s< s<refl ) ) | 159 ... | t with t (case2 (s< s<refl ) ) |
103 c3 lx (OSuc .lx x₁) d not | t | () | 160 c3 lx (OSuc .lx x₁) d not | t | () |
104 | 161 |
105 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z ∋ x | |
106 transitive {n} {z} {y} {x} z∋y x∋y with ordtrans {!!} {!!} | |
107 ... | t = lemma0 (lemma t) where | |
108 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord x) | |
109 lemma xo<z = {!!} | |
110 lemma0 : def ( ord→od ( od→ord z )) ( od→ord x) → def z (od→ord x) | |
111 lemma0 dz = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso) refl | |
112 | |
113 ∅5 : {n : Level} → { x : Ordinal {n} } → ¬ ( x ≡ o∅ {n} ) → o∅ {n} o< x | 162 ∅5 : {n : Level} → { x : Ordinal {n} } → ¬ ( x ≡ o∅ {n} ) → o∅ {n} o< x |
114 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) | 163 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) |
115 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ< | 164 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ< |
116 ∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n) | 165 ∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n) |
117 | 166 |
164 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso ))) | 213 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso ))) |
165 | 214 |
166 ≡-def : {n : Level} → { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } ) | 215 ≡-def : {n : Level} → { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } ) |
167 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where | 216 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where |
168 lemma : ord→od x == record { def = λ z → z o< x } | 217 lemma : ord→od x == record { def = λ z → z o< x } |
169 eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where | 218 eq→ lemma {w} lt = {!!} |
170 t : (od→ord ( ord→od w)) o< (od→ord (ord→od x)) | 219 -- ?subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where |
171 t = {!!} | 220 --t : (od→ord ( ord→od w)) o< (od→ord (ord→od x)) |
172 eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl | 221 --t = o<-subst lt ? ? |
222 eq← lemma {w} lt = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl | |
173 | 223 |
174 od≡-def : {n : Level} → { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } | 224 od≡-def : {n : Level} → { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } |
175 od≡-def {n} {x} = subst (λ k → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} )) | 225 od≡-def {n} {x} = subst (λ k → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} )) |
176 | 226 |
177 ==→o≡1 : {n : Level} → { x y : OD {suc n} } → x == y → od→ord x ≡ od→ord y | 227 ==→o≡1 : {n : Level} → { x y : OD {suc n} } → x == y → od→ord x ≡ od→ord y |
191 o<∋→ : {n : Level} → { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x | 241 o<∋→ : {n : Level} → { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x |
192 o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t where | 242 o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t where |
193 t : def (ord→od (od→ord a)) (od→ord x) | 243 t : def (ord→od (od→ord a)) (od→ord x) |
194 t = {!!} | 244 t = {!!} |
195 | 245 |
196 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} | 246 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅' {suc n} |
197 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} )) | 247 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅' {suc n} )) |
198 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where | 248 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where |
199 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥ | 249 lemma : o∅ {suc n } o< (od→ord (od∅' {suc n} )) → ⊥ |
200 lemma lt with def-subst {!!} oiso refl | 250 lemma lt with def-subst {suc n} {_} {_} {_} {_} ( o<→c< ( o<-subst lt (sym diso) refl ) ) refl diso |
201 lemma lt | t = {!!} | 251 lemma lt | t = {!!} |
202 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso | 252 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso |
203 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | 253 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) |
204 | 254 |
205 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y ) | 255 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y ) |
206 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt | 256 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt |
207 | 257 |
208 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) | 258 o<→¬c> : {n : Level} → { x y : Ordinal {n} } → x o< y → ¬ (y c< x ) |
209 o<→¬c> {n} {x} {y} olt clt = o<> olt {!!} where | 259 o<→¬c> {n} {x} {y} olt clt = o<> olt {!!} where |
210 | 260 |
211 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y | 261 o≡→¬c< : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ¬ x c< y |
212 o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) lt | 262 o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ x y {!!} {!!} |
213 | 263 |
214 tri-c< : {n : Level} → Trichotomous _==_ (_c<_ {suc n}) | 264 tri-c< : {n : Level} → Trichotomous _≡_ (_c<_ {suc n}) |
215 tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y) | 265 tri-c< {n} x y with trio< {n} x y |
216 tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) (o<→¬== a) ( o<→¬c> a ) | 266 tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) {!!} ( o<→¬c> a ) |
217 tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b)) | 267 tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) {!!} (o≡→¬c< (sym b)) |
218 tri-c< {n} x y | tri> ¬a ¬b c = tri> ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst {!!} oiso refl) | 268 tri-c< {n} x y | tri> ¬a ¬b c = tri> ( o<→¬c> c) (λ eq → {!!} ) (def-subst {!!} oiso refl) |
219 | 269 |
220 c<> : {n : Level } { x y : OD {suc n}} → x c< y → y c< x → ⊥ | 270 c<> : {n : Level } { x y : Ordinal {suc n}} → x c< y → y c< x → ⊥ |
221 c<> {n} {x} {y} x<y y<x with tri-c< x y | 271 c<> {n} {x} {y} x<y y<x with tri-c< x y |
222 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x | 272 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x |
223 c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b x<y | 273 c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> {!!} {!!} |
224 c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y | 274 c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y |
225 | 275 |
226 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} ) | 276 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} ) |
227 ∅< {n} {x} {y} d eq with eq→ eq d | 277 ∅< {n} {x} {y} d eq with eq→ eq d |
228 ∅< {n} {x} {y} d eq | lift () | 278 ∅< {n} {x} {y} d eq | lift () |
229 | 279 |
230 ∅6 : {n : Level} → { x : OD {suc n} } → ¬ ( x ∋ x ) -- no Russel paradox | 280 ∅6 : {n : Level} → { x : OD {suc n} } → ¬ ( x ∋ x ) -- no Russel paradox |
231 ∅6 {n} {x} x∋x = c<> {n} {x} {x} {!!} {!!} | 281 ∅6 {n} {x} x∋x = c<> {n} {{!!}} {{!!}} {!!} {!!} |
232 | 282 |
233 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y → (def A y → def B y) → def A x → def B x | 283 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y → (def A y → def B y) → def A x → def B x |
234 def-iso refl t = t | 284 def-iso refl t = t |
235 | |
236 is-∋ : {n : Level} → ( x y : OD {suc n} ) → Dec ( x ∋ y ) | |
237 is-∋ {n} x y with tri-c< x y | |
238 is-∋ {n} x y | tri< a ¬b ¬c = no {!!} | |
239 is-∋ {n} x y | tri≈ ¬a b ¬c = no {!!} | |
240 is-∋ {n} x y | tri> ¬a ¬b c = yes {!!} | |
241 | 285 |
242 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) | 286 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) |
243 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl | 287 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl |
244 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) | 288 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) |
245 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) | 289 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) |
250 ¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where | 294 ¬∅=→∅∈ {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where |
251 lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} | 295 lemma : (ox : Ordinal {suc n}) → ¬ (ord→od ox == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} |
252 lemma ox ne with is-o∅ ox | 296 lemma ox ne with is-o∅ ox |
253 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where | 297 lemma ox ne | yes refl with ne ( ord→== lemma1 ) where |
254 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ | 298 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ |
255 lemma1 = cong ( λ k → od→ord k ) o∅≡od∅ | 299 lemma1 = cong ( λ k → od→ord k ) {!!} |
256 lemma o∅ ne | yes refl | () | 300 lemma o∅ ne | yes refl | () |
257 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ {!!} | 301 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) {!!} {!!} |
258 | 302 |
259 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | 303 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
260 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) | 304 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) |
261 | 305 |
262 csuc : {n : Level} → OD {suc n} → OD {suc n} | 306 csuc : {n : Level} → OD {suc n} → OD {suc n} |
266 | 310 |
267 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} | 311 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} |
268 ZFSubset A x = record { def = λ y → def A y ∧ def x y } | 312 ZFSubset A x = record { def = λ y → def A y ∧ def x y } |
269 | 313 |
270 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} | 314 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} |
271 Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | 315 Def {n} A = record { def = λ y → y o< ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )))) } |
272 | 316 |
273 -- Constructible Set on α | 317 -- Constructible Set on α |
274 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n} | 318 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n} |
275 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ | 319 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ |
276 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) | 320 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) |
277 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) | 321 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) |
278 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) } | 322 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) } |
279 | 323 |
280 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 324 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
281 OD→ZF {n} = record { | 325 OD→ZF {n} = record { |
282 ZFSet = OD {suc n} | 326 ZFSet = OD {suc n} |
283 ; _∋_ = _∋_ | 327 ; _∋_ = _∋_ |
394 } | 438 } |
395 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x | 439 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x |
396 replacement {ψ} X x = sup-c< ψ {x} | 440 replacement {ψ} X x = sup-c< ψ {x} |
397 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) | 441 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) |
398 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq | 442 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq |
399 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} | |
400 minimul x not = od∅ | |
401 regularity : (x : OD) (not : ¬ (x == od∅)) → | 443 regularity : (x : OD) (not : ¬ (x == od∅)) → |
402 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) | 444 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
403 proj1 (regularity x not ) = ¬∅=→∅∈ not | 445 proj1 (regularity x not ) = x∋minimul x not |
404 proj2 (regularity x not ) = record { eq→ = reg ; eq← = λ () } where | 446 proj2 (regularity x not ) = record { eq→ = reg ; eq← = λ () } where |
405 reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y | 447 reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y |
406 reg {y} t with proj1 t | 448 reg {y} t with minimul-1 x not (ord→od y) (proj2 t ) |
407 ... | x∈∅ = x∈∅ | 449 ... | t1 = lift t1 |
408 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B | 450 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B |
409 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d | 451 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d |
410 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d | 452 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d |
411 xx-union : {x : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) } | 453 xx-union : {x : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) } |
412 xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x)) | 454 xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x)) |
430 omega = record { lv = Suc Zero ; ord = Φ 1 } | 472 omega = record { lv = Suc Zero ; ord = Φ 1 } |
431 infinite : OD {suc n} | 473 infinite : OD {suc n} |
432 infinite = ord→od ( omega ) | 474 infinite = ord→od ( omega ) |
433 infinity∅ : ord→od ( omega ) ∋ od∅ {suc n} | 475 infinity∅ : ord→od ( omega ) ∋ od∅ {suc n} |
434 infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅} | 476 infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅} |
435 {!!} refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k → od→ord k) o∅≡od∅ )) | 477 {!!} refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k → od→ord k) {!!} )) |
436 infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega | 478 infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega |
437 infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where | 479 infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where |
438 t : od→ord x o< od→ord (ord→od (omega)) | 480 t : od→ord x o< od→ord (ord→od (omega)) |
439 t = ∋→o< {n} {infinite} {x} lt | 481 t = ∋→o< {n} {infinite} {x} lt |
440 infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x )) | 482 infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x )) |