Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/src/ordinal.agda Mon Jul 11 05:50:49 2022 +0900 +++ b/src/ordinal.agda Mon Jul 11 11:49:11 2022 +0900 @@ -200,12 +200,12 @@ lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 -OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1 -OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (NP.<-irrelevant _ _ ) -OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) -OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) -OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl -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 +OrdIrr : {n : Level } {x y : Ordinal {suc n} } (lt lt1 : x o< y) → lt ≡ lt1 +OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case1 x₁) = cong case1 (NP.<-irrelevant _ _ ) +OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case1 x) (case2 x₁) = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x ) +OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} (case2 x) (case1 x₁) = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ ) +OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} (case2 Φ<) (case2 Φ<) = refl +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 lemma1 : {lx : ℕ} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )