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

comparison ordinal.agda @ 423:9984cdd88da3

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, 01 Aug 2020 18:05:23 +0900
parents 44a484f17f26
children cc7909f86841
comparison
equal deleted inserted replaced
422:44a484f17f26 423:9984cdd88da3
1 open import Level 1 open import Level
2 module ordinal where 2 module ordinal where
3 3
4 open import zf 4 open import logic
5 5 open import nat
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 open import Data.Empty 7 open import Data.Empty
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 open import logic 9 open import Data.Nat.Properties
10 open import nat 10 open import Relation.Nullary
11 open import Relation.Binary.Core
12
11 13
12 data OrdinalD {n : Level} : (lv : Nat) → Set n where 14 data OrdinalD {n : Level} : (lv : Nat) → Set n where
13 Φ : (lv : Nat) → OrdinalD lv 15 Φ : (lv : Nat) → OrdinalD lv
14 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv 16 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
15 17
37 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< () 39 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
38 40
39 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y 41 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y
40 d<→lv Φ< = refl 42 d<→lv Φ< = refl
41 d<→lv (s< lt) = refl 43 d<→lv (s< lt) = refl
42
43 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x
44 o<-subst df refl refl = df
45
46 open import Data.Nat.Properties
47 open import Data.Unit using ( ⊤ )
48 open import Relation.Nullary
49
50 open import Relation.Binary
51 open import Relation.Binary.Core
52 44
53 o∅ : {n : Level} → Ordinal {n} 45 o∅ : {n : Level} → Ordinal {n}
54 o∅ = record { lv = Zero ; ord = Φ Zero } 46 o∅ = record { lv = Zero ; ord = Φ Zero }
55 47
56 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl) 48 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
205 197
206 open import Ordinals 198 open import Ordinals
207 199
208 C-Ordinal : {n : Level} → Ordinals {suc n} 200 C-Ordinal : {n : Level} → Ordinals {suc n}
209 C-Ordinal {n} = record { 201 C-Ordinal {n} = record {
210 ord = Ordinal {suc n} 202 Ordinal = Ordinal {suc n}
211 ; o∅ = o∅ 203 ; o∅ = o∅
212 ; osuc = osuc 204 ; osuc = osuc
213 ; _o<_ = _o<_ 205 ; _o<_ = _o<_
214 ; next = next 206 ; next = next
215 ; isOrdinal = record { 207 ; isOrdinal = record {
216 Otrans = ordtrans 208 ordtrans = ordtrans
217 ; OTri = trio< 209 ; trio< = trio<
218 ; ¬x<0 = ¬x<0 210 ; ¬x<0 = ¬x<0
219 ; <-osuc = <-osuc 211 ; <-osuc = <-osuc
220 ; osuc-≡< = osuc-≡< 212 ; osuc-≡< = osuc-≡<
221 ; TransFinite = TransFinite1 213 ; TransFinite = TransFinite1
222 ; TransFinite1 = TransFinite2 214 ; TransFinite1 = TransFinite2