Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 173:e6e1bdbda450
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 15:28:20 +0900 |
parents | 8c4d1423d7c4 |
children | ad7a6185b6d5 |
comparison
equal
deleted
inserted
replaced
172:8c4d1423d7c4 | 173:e6e1bdbda450 |
---|---|
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 (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where | 245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where |
246 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } | 246 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly } |
283 lemma z lt | case2 lz=ly with <-cmp lx ly | 283 lemma z lt | case2 lz=ly with <-cmp lx ly |
284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | 284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen |
285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) | 285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) |
286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | 286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) |
287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) | 287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) |
288 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord (Suc lx) (Φ (Suc lx)) {_} {ord (od→ord z)} | 288 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx |
289 (case1 (subst (λ k → k < Suc lx) (trans (sym lemma1) (sym eq)) lemma2 ))) | 289 (ox lz=ly -- ord (od→ord z) d< ord (od→ord (ord→od (record { lv = lx ; ord = oy }))) |
290 (subst (λ k → lv (od→ord z) ≡ k ) lemma1 eq) ) {_} {ord (od→ord z)} (case2 {!!})) where | |
291 ox : {lx lz : Nat} → {oy : OrdinalD {suc n} lz} {oz : OrdinalD {suc n} lx} → {!!} d< {!!} → lz ≡ lx → OrdinalD {suc n} lx | |
292 ox = ? | |
290 | 293 |
291 | 294 |
292 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 295 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
293 OD→ZF {n} = record { | 296 OD→ZF {n} = record { |
294 ZFSet = OD {suc n} | 297 ZFSet = OD {suc n} |