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

comparison Ordinals.agda @ 388:19687f3304c9

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, 25 Jul 2020 12:54:28 +0900
parents 8b0715e28b33
children 43b0a6ca7602
comparison
equal deleted inserted replaced
387:8b0715e28b33 388:19687f3304c9
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 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) 23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
24 TransFinite : { ψ : ord → Set n } 24 TransFinite : { ψ : ord → Set n }
25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
26 → ∀ (x : ord) → ψ x 26 → ∀ (x : ord) → ψ x
27 TransFinite1 : { ψ : ord → Set (suc n) }
28 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
29 → ∀ (x : ord) → ψ x
27 30
28 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 31 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
29 field 32 field
30 x<nx : { y : ord } → (y o< next y ) 33 x<nx : { y : ord } → (y o< next y )
31 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 34 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
60 63
61 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 64 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
62 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 65 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
63 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 66 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
64 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) 67 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
68 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O)
65 69
66 x<nx = IsNext.x<nx (Ordinals.isNext O) 70 x<nx = IsNext.x<nx (Ordinals.isNext O)
67 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 71 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
68 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) 72 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O)
69 73