Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 271:2169d948159b
fix incl
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 30 Dec 2019 23:45:59 +0900 |
parents | 30e419a2be24 |
children | 6f10c47e4e7a |
comparison
equal
deleted
inserted
replaced
270:fc3d4bc1dc5e | 271:2169d948159b |
---|---|
237 | 237 |
238 import OD | 238 import OD |
239 -- open inOrdinal C-Ordinal | 239 -- open inOrdinal C-Ordinal |
240 open OD (C-Ordinal {n}) | 240 open OD (C-Ordinal {n}) |
241 open OD.OD | 241 open OD.OD |
242 | 242 open _⊆_ |
243 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z} | 243 |
244 o<→c< lt lt1 = ordtrans lt1 lt | 244 o<→c< : {x y : Ordinal } → x o< y → Ord x ⊆ Ord y |
245 | 245 o<→c< lt = record { incl = λ lt1 → ordtrans lt1 lt } |
246 ⊆→o< : {x y : Ordinal } → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y | 246 |
247 ⊆→o< : {x y : Ordinal } → Ord x ⊆ Ord y → x o< osuc y | |
247 ⊆→o< {x} {y} lt with trio< x y | 248 ⊆→o< {x} {y} lt with trio< x y |
248 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc | 249 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc |
249 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc | 250 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc |
250 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) | 251 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with incl lt (o<-subst c (sym diso) refl ) |
251 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) | 252 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) |
252 | 253 |
253 -- ZFSubset : (A x : OD ) → OD | 254 -- ZFSubset : (A x : OD ) → OD |
254 -- ZFSubset A x = record { def = λ y → def A y ∧ def x y } | 255 -- ZFSubset A x = record { def = λ y → def A y ∧ def x y } |
255 | 256 |
256 -- Def : (A : OD ) → OD | 257 -- Def : (A : OD ) → OD |
257 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | 258 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) |
258 | 259 |
259 Ord-lemma : (a : Ordinal) (x : OD) → _⊆_ (ord→od a) (Ord a) {x} | 260 Ord-lemma : (a : Ordinal) → ord→od a ⊆ Ord a |
260 Ord-lemma a x lt = o<-subst (c<→o< lt ) refl diso | 261 Ord-lemma a = record { incl = λ lt → o<-subst (c<→o< lt ) refl diso } |
261 | 262 |
262 ⊆-trans : {a b c x : OD} → _⊆_ a b {x} → _⊆_ b c {x} → _⊆_ a c {x} | 263 ⊆-trans : {a b c x : OD} → a ⊆ b → b ⊆ c → a ⊆ c |
263 ⊆-trans a⊆b b⊆c a∋x = b⊆c (a⊆b a∋x) | 264 ⊆-trans a⊆b b⊆c = record { incl = λ a∋x → incl b⊆c (incl a⊆b a∋x) } |
264 | 265 |
265 _∩_ = IsZF._∩_ isZF | 266 _∩_ = IsZF._∩_ isZF |
266 | 267 |
267 -- | 268 -- |
268 -- ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a) | 269 -- ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a) |