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

comparison Ordinals.agda @ 320:21203fe0342f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
infinite ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Jul 2020 21:58:01 +0900
parents d4802179a66f
children a81824502ebd
comparison
equal deleted inserted replaced
319:eef432aa8dfb 320:21203fe0342f
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 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where 16 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
17 field 17 field
18 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
19 OTri : Trichotomous {n} _≡_ _o<_ 19 OTri : Trichotomous {n} _≡_ _o<_
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 : { x : ord } → (x o< next x )∧ (¬ ((y : ord) → next x ≡ osuc y) )
24 TransFinite : { ψ : ord → Set (suc n) } 25 TransFinite : { ψ : ord → Set (suc n) }
25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
26 → ∀ (x : ord) → ψ x 27 → ∀ (x : ord) → ψ x
27 28
28 29
30 field 31 field
31 ord : Set n 32 ord : Set n
32 o∅ : ord 33 o∅ : ord
33 osuc : ord → ord 34 osuc : ord → ord
34 _o<_ : ord → ord → Set n 35 _o<_ : ord → ord → Set n
35 isOrdinal : IsOrdinals ord o∅ osuc _o<_ 36 next : ord → ord
37 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
36 38
37 module inOrdinal {n : Level} (O : Ordinals {n} ) where 39 module inOrdinal {n : Level} (O : Ordinals {n} ) where
38 40
39 Ordinal : Set n 41 Ordinal : Set n
40 Ordinal = Ordinals.ord O 42 Ordinal = Ordinals.ord O
45 osuc : Ordinal → Ordinal 47 osuc : Ordinal → Ordinal
46 osuc = Ordinals.osuc O 48 osuc = Ordinals.osuc O
47 49
48 o∅ : Ordinal 50 o∅ : Ordinal
49 o∅ = Ordinals.o∅ O 51 o∅ = Ordinals.o∅ O
52
53 next : Ordinal → Ordinal
54 next = Ordinals.next O
50 55
51 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O) 56 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
52 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O) 57 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
53 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O) 58 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
54 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O) 59 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
60 next-limit = IsOrdinals.next-limit (Ordinals.isOrdinal O)
55 61
56 o<-dom : { x y : Ordinal } → x o< y → Ordinal 62 o<-dom : { x y : Ordinal } → x o< y → Ordinal
57 o<-dom {x} _ = x 63 o<-dom {x} _ = x
58 64
59 o<-cod : { x y : Ordinal } → x o< y → Ordinal 65 o<-cod : { x y : Ordinal } → x o< y → Ordinal