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

comparison src/Ordinals.agda @ 431:a5f8084b8368

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reorganiztion for apkg
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Dec 2020 10:23:37 +0900
parents
children 099ca2fea51c
comparison
equal deleted inserted replaced
430:28c7be8f252c 431:a5f8084b8368
1 open import Level
2 module Ordinals where
3
4 open import zf
5
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 open import Data.Empty
8 open import Relation.Binary.PropositionalEquality
9 open import logic
10 open import nat
11 open import Data.Unit using ( ⊤ )
12 open import Relation.Nullary
13 open import Relation.Binary
14 open import Relation.Binary.Core
15
16 record Oprev {n : Level} (ord : Set n) (osuc : ord → ord ) (x : ord ) : Set (suc n) where
17 field
18 oprev : ord
19 oprev=x : osuc oprev ≡ x
20
21 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
22 field
23 ordtrans : {x y z : ord } → x o< y → y o< z → x o< z
24 trio< : Trichotomous {n} _≡_ _o<_
25 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
26 <-osuc : { x : ord } → x o< osuc x
27 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
28 Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x )
29 TransFinite : { ψ : ord → Set (suc n) }
30 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
31 → ∀ (x : ord) → ψ x
32
33
34 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
35 field
36 x<nx : { y : ord } → (y o< next y )
37 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
38 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
39
40 record Ordinals {n : Level} : Set (suc (suc n)) where
41 field
42 Ordinal : Set n
43 o∅ : Ordinal
44 osuc : Ordinal → Ordinal
45 _o<_ : Ordinal → Ordinal → Set n
46 next : Ordinal → Ordinal
47 isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
48 isNext : IsNext Ordinal o∅ osuc _o<_ next
49
50 module inOrdinal {n : Level} (O : Ordinals {n} ) where
51
52 open Ordinals O
53 open IsOrdinals isOrdinal
54 open IsNext isNext
55
56 TransFinite0 : { ψ : Ordinal → Set n }
57 → ( (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x )
58 → ∀ (x : Ordinal) → ψ x
59 TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
60 ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
61 ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))
62