Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 185:a002ce0346dd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2019 18:36:45 +0900 |
| parents | 65e1b2e415bb |
| children | 914cc522c53a |
| files | OD.agda |
| diffstat | 1 files changed, 0 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/OD.agda Mon Jul 22 17:31:52 2019 +0900 +++ b/OD.agda Mon Jul 22 18:36:45 2019 +0900 @@ -525,22 +525,3 @@ lx ≡ ly → ly ≡ lv (od→ord z) → ψ z lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl) - ==→o≡' : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y - ==→o≡' {n} {x} {y} eq = lemma1 {!!} where - lemma4 : { x y : OD {suc n} } → (x == y) → ¬ ( od→ord x o< od→ord y ) - lemma4 = {!!} - lemma3 : { x y : OD {suc n} } → (x == y) → od→ord x ≡ od→ord y - -- x < y - -- m m - lemma3 {x} {y} eq with trio< (od→ord x) (od→ord y) - lemma3 {x} {y} eq | tri≈ ¬a b ¬c = b - lemma3 {x} {y} eq | tri< a ¬b ¬c = {!!} - lemma3 {x} {y} eq | tri> ¬a ¬b c = {!!} - lemma1 : { x y : OD {suc n} } → Ord (od→ord x) == Ord (od→ord y) → x ≡ y - lemma1 {x} {y} eq = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k ) lemma2) where - lemma2 : (od→ord x) ≡ (od→ord y) - lemma2 with trio< (od→ord x) (od→ord y) - lemma2 | tri≈ ¬a b ¬c = b - lemma2 | tri< a ¬b ¬c with eq← eq a - ... | lt = ⊥-elim ( o<¬≡ refl lt ) - lemma2 | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl ( eq→ eq c ))