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

comparison 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
comparison
equal deleted inserted replaced
38:20cddbb2fc90 39:457e6626e0b1
49 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x 49 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
50 s<refl {n} {lv} {Φ lv} = Φ< 50 s<refl {n} {lv} {Φ lv} = Φ<
51 s<refl {n} {lv} {OSuc lv x} = s< s<refl 51 s<refl {n} {lv} {OSuc lv x} = s< s<refl
52 s<refl {n} {Suc lv} {ℵ lv} = ℵs< 52 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
53 53
54 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
55
56 ordinal-cong : {n : Level} {x y : Ordinal {n}} →
57 lv x ≡ lv y → ord x ≅ ord y → x ≡ y
58 ordinal-cong refl refl = refl
54 59
55 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ 60 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥
56 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t 61 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
57 62
58 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ 63 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥