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

comparison Ordinals.agda @ 324:fbabb20f222e

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 Sat, 04 Jul 2020 18:18:17 +0900
parents a81824502ebd
children feeba7fd499a
comparison
equal deleted inserted replaced
323:e228e96965f0 324:fbabb20f222e
20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
21 <-osuc : { x : ord } → x o< osuc x 21 <-osuc : { x : ord } → x o< osuc x
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
23 is-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) ) 23 is-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) 24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y )
25 TransFinite : { ψ : ord → Set (suc n) } 25 TransFinite : { ψ : ord → Set n }
26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
27 → ∀ (x : ord) → ψ x 27 → ∀ (x : ord) → ψ x
28 28
29 29
30 record Ordinals {n : Level} : Set (suc (suc n)) where 30 record Ordinals {n : Level} : Set (suc (suc n)) where