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

comparison ordinal.agda @ 70:cd9cf8b09610

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union needs +1 space
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Jun 2019 10:01:38 +0900
parents e584686a1307
children d088eb66564e
comparison
equal deleted inserted replaced
69:93abc0133b8a 70:cd9cf8b09610
20 20
21 data ¬ℵ {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where 21 data ¬ℵ {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where
22 ¬ℵΦ : ¬ℵ (Φ lx) 22 ¬ℵΦ : ¬ℵ (Φ lx)
23 ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) 23 ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x)
24 24
25 --
26 -- Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ... < ℵ (Suc lv)
27 --
25 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where 28 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
26 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x 29 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
27 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y 30 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
28 ℵΦ< : {lx : Nat} → Φ (Suc lx) d< (ℵ lx) 31 ℵΦ< : {lx : Nat} → Φ (Suc lx) d< (ℵ lx)
29 ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x → OSuc (Suc lx) x d< (ℵ lx) 32 ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x → OSuc (Suc lx) x d< (ℵ lx)