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

diff ordinal.agda @ 39:457e6626e0b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 May 2019 19:48:51 +0900
parents 88b77cecaeba
children b60db5903f01
line wrap: on
line diff
--- a/ordinal.agda	Thu May 23 14:20:35 2019 +0900
+++ b/ordinal.agda	Thu May 23 19:48:51 2019 +0900
@@ -51,6 +51,11 @@
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
 
+open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
+
+ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
+      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
+ordinal-cong refl refl = refl
 
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t