Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/ordinal.agda @ 693:a3b7f1e0ca60
same problem again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Jul 2022 11:49:11 +0900 |
| parents | 4186c0331abb |
| children | 7c39cae23803 |
comparison
equal
deleted
inserted
replaced
| 692:38103b4e6780 | 693:a3b7f1e0ca60 |
|---|---|
| 198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y | 198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y |
| 199 lemma y lt with osuc-≡< lt | 199 lemma y lt with osuc-≡< lt |
| 200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) | 200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) |
| 201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 | 201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 |
| 202 | 202 |
| 203 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1 | 203 OrdIrr : {n : Level } {x y : Ordinal {suc n} } (lt lt1 : x o< y) → lt ≡ lt1 |
| 204 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ ) | 204 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case1 x₁) = cong case1 (NP.<-irrelevant _ _ ) |
| 205 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) | 205 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case2 x₁) = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) |
| 206 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) | 206 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case2 x) (case1 x₁) = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) |
| 207 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl | 207 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} (case2 Φ<) (case2 Φ<) = refl |
| 208 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where | 208 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} (case2 (s< x)) (case2 (s< x₁)) = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where |
| 209 lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y | 209 lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y |
| 210 lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl | 210 lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl |
| 211 lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y ) | 211 lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y ) |
| 212 | 212 |
| 213 TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m } | 213 TransFinite3 : {n m : Level} { ψ : Ordinal {suc n} → Set m } |