Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 171:729b80df8a8a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 08:34:36 +0900 |
parents | c96f28c3c387 |
children | 8c4d1423d7c4 |
comparison
equal
deleted
inserted
replaced
170:c96f28c3c387 | 171:729b80df8a8a |
---|---|
236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α | 236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α |
237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x | 237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x |
238 | 238 |
239 -- another form of regularity | 239 -- another form of regularity |
240 -- | 240 -- |
241 {-# TERMINATING #-} | 241 -- {-# TERMINATING #-} |
242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |
244 → (x : OD {suc n} ) → ψ x | 244 → (x : OD {suc n} ) → ψ x |
245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where | 245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where |
246 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) | 246 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) |
250 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where | 250 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where |
251 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } | 251 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } |
252 lemma y lt with osuc-≡< y<x | 252 lemma y lt with osuc-≡< y<x |
253 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso | 253 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso |
254 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | 254 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 |
255 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = oy }} (case1 (s≤s x)) with <-cmp lx ly | 255 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {oy} = |
256 ... | tri< a ¬b ¬c = ⊥-elim (lemma a x ) where | 256 TransFinite {suc n} {suc n ⊔ m} {λ x → x o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od x)} lemma1 lemma2 oy where |
257 lemma : {lx ly : Nat} → Suc lx ≤ ly → ly ≤ lx → ⊥ | 257 lemma1 : (ly : Nat) → |
258 lemma (s≤s lt1) (s≤s lt2) = lemma lt1 lt2 | 258 record { lv = ly ; ord = Φ ly } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → |
259 ... | tri≈ ¬a refl ¬c = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso ? | 259 ψ (ord→od (record { lv = ly ; ord = Φ ly })) |
260 ... | tri> ¬a ¬b c = ε-induction-ord record { lv = lx ; ord = (Φ lx) } (case1 c) | 260 lemma1 ly lt = ind {!!} |
261 lemma2 : (ly : Nat) (oy : OrdinalD ly) → | |
262 (record { lv = ly ; ord = oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = oy }))) → | |
263 record { lv = ly ; ord = OSuc ly oy } o< record { lv = Suc lx ; ord = Φ (Suc lx) } → ψ (ord→od (record { lv = ly ; ord = OSuc ly oy })) | |
264 lemma2 ly oy p lt = ind {!!} | |
261 | 265 |
262 | 266 |
263 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 267 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
264 OD→ZF {n} = record { | 268 OD→ZF {n} = record { |
265 ZFSet = OD {suc n} | 269 ZFSet = OD {suc n} |