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

comparison src/Ordinals.agda @ 1286:619e68271cf8

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 Mon, 22 May 2023 19:06:25 +0900
parents 45cd80181a29
children
comparison
equal deleted inserted replaced
1285:302cfb533201 1286:619e68271cf8
31 31
32 32
33 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where 33 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
34 field 34 field
35 x<nx : { y : ord } → (y o< next y ) 35 x<nx : { y : ord } → (y o< next y )
36 nexto≡ : {x : ord} → next x ≡ next (osuc x)
36 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 37 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
37 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
38 38
39 record Ordinals {n : Level} : Set (suc (suc n)) where 39 record Ordinals {n : Level} : Set (suc (suc n)) where
40 field 40 field
41 Ordinal : Set n 41 Ordinal : Set n
42 o∅ : Ordinal 42 o∅ : Ordinal