Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 79:c07c548b2ac1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 10:50:03 +0900
parents 9a7a64b2388c
children 461690d60d07
files ordinal-definable.agda
diffstat 1 files changed, 7 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Mon Jun 03 10:19:52 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 03 10:50:03 2019 +0900
@@ -183,6 +183,12 @@
 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
 ... | ()
 
+==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } → ord→od x == ord→od y →  x ≡ y 
+==→o≡ {n} {x} {y} eq with trio< {n} x y
+==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
+==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
+==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
+
 o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
@@ -237,7 +243,7 @@
      lemma o∅ ne | yes refl | ()
      lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))  
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record {