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

comparison Ordinals.agda @ 222:59771eb07df0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TransFinite induction fixed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Aug 2019 16:54:30 +0900
parents 1709c80b7275
children 846e0926bb89
comparison
equal deleted inserted replaced
221:1709c80b7275 222:59771eb07df0
11 open import Data.Unit using ( ⊤ ) 11 open import Data.Unit using ( ⊤ )
12 open import Relation.Nullary 12 open import Relation.Nullary
13 open import Relation.Binary 13 open import Relation.Binary
14 open import Relation.Binary.Core 14 open import Relation.Binary.Core
15 15
16 16 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
17
18 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set n where
19 field 17 field
20 Otrans : {x y z : ord } → x o< y → y o< z → x o< z 18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
21 OTri : Trichotomous {n} _≡_ _o<_ 19 OTri : Trichotomous {n} _≡_ _o<_
22 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
23 <-osuc : { x : ord } → x o< osuc x 21 <-osuc : { x : ord } → x o< osuc x
24 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)
25 23 TransFinite : { ψ : ord → Set (suc n) }
26 record Ordinals {n : Level} : Set (suc n) where 24 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
25 → ∀ (x : ord) → ψ x
26
27
28 record Ordinals {n : Level} : Set (suc (suc n)) where
27 field 29 field
28 ord : Set n 30 ord : Set n
29 o∅ : ord 31 o∅ : ord
30 osuc : ord → ord 32 osuc : ord → ord
31 _o<_ : ord → ord → Set n 33 _o<_ : ord → ord → Set n