annotate Ordinals.agda @ 403:ce2ce3f62023

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 10:51:08 +0900
parents 43b0a6ca7602
children 6dcea4c7cba1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
1 open import Level
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
2 module Ordinals where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
4 open import zf
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
75
714470702a8b Union done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
7 open import Data.Empty
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
8 open import Relation.Binary.PropositionalEquality
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 204
diff changeset
9 open import logic
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 204
diff changeset
10 open import nat
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
11 open import Data.Unit using ( ⊤ )
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
12 open import Relation.Nullary
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
13 open import Relation.Binary
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
14 open import Relation.Binary.Core
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
320
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
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
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
17 field
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
18 Otrans : {x y z : ord } → x o< y → y o< z → x o< z
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
19 OTri : Trichotomous {n} _≡_ _o<_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
21 <-osuc : { x : ord } → x o< osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
23 not-limit-p : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
324
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 321
diff changeset
24 TransFinite : { ψ : ord → Set n }
222
59771eb07df0 TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
25 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
59771eb07df0 TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
26 → ∀ (x : ord) → ψ x
388
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
27 TransFinite1 : { ψ : ord → Set (suc n) }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
28 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
29 → ∀ (x : ord) → ψ x
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
30
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
31 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
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
32 field
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
33 x<nx : { y : ord } → (y o< next y )
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
34 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
35 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
222
59771eb07df0 TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
36
59771eb07df0 TransFinite induction fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
37 record Ordinals {n : Level} : Set (suc (suc n)) where
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
38 field
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
39 ord : Set n
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
40 o∅ : ord
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
41 osuc : ord → ord
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
42 _o<_ : ord → ord → Set n
320
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
43 next : ord → ord
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
44 isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
45 isNext : IsNext ord o∅ osuc _o<_ next
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
46
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
47 module inOrdinal {n : Level} (O : Ordinals {n} ) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
49 Ordinal : Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
50 Ordinal = Ordinals.ord O
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
51
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
52 _o<_ : Ordinal → Ordinal → Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
53 _o<_ = Ordinals._o<_ O
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
54
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
55 osuc : Ordinal → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
56 osuc = Ordinals.osuc O
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
57
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
58 o∅ : Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
59 o∅ = Ordinals.o∅ O
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
60
320
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
61 next : Ordinal → Ordinal
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
62 next = Ordinals.next O
21203fe0342f infinite ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
63
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
64 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
65 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
66 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal O)
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 222
diff changeset
67 TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
388
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 387
diff changeset
68 TransFinite1 = IsOrdinals.TransFinite1 (Ordinals.isOrdinal O)
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
69
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
70 x<nx = IsNext.x<nx (Ordinals.isNext O)
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
71 osuc<nx = IsNext.osuc<nx (Ordinals.isNext O)
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
72 ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O)
321
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 320
diff changeset
73
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
74 o<-dom : { x y : Ordinal } → x o< y → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
75 o<-dom {x} _ = x
74
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
76
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
77 o<-cod : { x y : Ordinal } → x o< y → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
78 o<-cod {_} {y} _ = y
147
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 144
diff changeset
79
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
80 o<-subst : {Z X z x : Ordinal } → Z o< X → Z ≡ z → X ≡ x → z o< x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
81 o<-subst df refl refl = df
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
82
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
83 ordtrans : {x y z : Ordinal } → x o< y → y o< z → x o< z
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
84 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O)
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
85
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
86 trio< : Trichotomous _≡_ _o<_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
87 trio< = IsOrdinals.OTri (Ordinals.isOrdinal O)
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
88
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
89 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
90 o<¬≡ {ox} {oy} eq lt with trio< ox oy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
91 o<¬≡ {ox} {oy} eq lt | tri< a ¬b ¬c = ¬b eq
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
92 o<¬≡ {ox} {oy} eq lt | tri≈ ¬a b ¬c = ¬a lt
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
93 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
94
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
95 o<> : {x y : Ordinal } → y o< x → x o< y → ⊥
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
96 o<> {ox} {oy} lt tl with trio< ox oy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
97 o<> {ox} {oy} lt tl | tri< a ¬b ¬c = ¬c lt
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
98 o<> {ox} {oy} lt tl | tri≈ ¬a b ¬c = ¬a tl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
99 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
100
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
101 osuc-< : { x y : Ordinal } → y o< osuc x → x o< y → ⊥
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
102 osuc-< {x} {y} y<ox x<y with osuc-≡< y<ox
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
103 osuc-< {x} {y} y<ox x<y | case1 refl = o<¬≡ refl x<y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
104 osuc-< {x} {y} y<ox x<y | case2 y<x = o<> x<y y<x
180
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
105
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
106 osucc : {ox oy : Ordinal } → oy o< ox → osuc oy o< osuc ox
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
107 ---- y < osuc y < x < osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
108 ---- y < osuc y = x < osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
109 ---- y < osuc y > x < osuc x -> y = x ∨ x < y → ⊥
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
110 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
111 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
112 osucc {ox} {oy} oy<ox | tri≈ ¬a refl ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
113 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c with osuc-≡< c
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
114 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
115 osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
116
338
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
117 osucprev : {ox oy : Ordinal } → osuc oy o< osuc ox → oy o< ox
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
118 osucprev {ox} {oy} oy<ox with trio< oy ox
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
119 osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
120 osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
121 osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 330
diff changeset
122
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
123 open _∧_
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
124
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
125 osuc2 : ( x y : Ordinal ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
126 proj2 (osuc2 x y) lt = osucc lt
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
127 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
128 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
129 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
130
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
131 _o≤_ : Ordinal → Ordinal → Set n
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
132 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b )
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
133
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
134
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
135 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
136 xo<ab {oa} {ob} a→b with trio< oa ob
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
137 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
138 xo<ab {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
139 xo<ab {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) )
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
140
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
141 maxα : Ordinal → Ordinal → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
142 maxα x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
143 maxα x y | tri< a ¬b ¬c = y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
144 maxα x y | tri> ¬a ¬b c = x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
145 maxα x y | tri≈ ¬a refl ¬c = x
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
146
308
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
147 omin : Ordinal → Ordinal → Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
148 omin x y with trio< x y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
149 omin x y | tri< a ¬b ¬c = x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
150 omin x y | tri> ¬a ¬b c = y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
151 omin x y | tri≈ ¬a refl ¬c = x
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
152
308
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 302
diff changeset
153 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< omin x y
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
154 min1 {x} {y} {z} z<x z<y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
155 min1 {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
156 min1 {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
157 min1 {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
158
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
159 --
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
160 -- max ( osuc x , osuc y )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
161 --
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
162
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
163 omax : ( x y : Ordinal ) → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
164 omax x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
165 omax x y | tri< a ¬b ¬c = osuc y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
166 omax x y | tri> ¬a ¬b c = osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
167 omax x y | tri≈ ¬a refl ¬c = osuc x
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
168
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
169 omax< : ( x y : Ordinal ) → x o< y → osuc y ≡ omax x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
170 omax< x y lt with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
171 omax< x y lt | tri< a ¬b ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
172 omax< x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
173 omax< x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
174
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
175 omax≡ : ( x y : Ordinal ) → x ≡ y → osuc y ≡ omax x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
176 omax≡ x y eq with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
177 omax≡ x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
178 omax≡ x y eq | tri≈ ¬a refl ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
179 omax≡ x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
91
b4742cf4ef97 infinity axiom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
180
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
181 omax-x : ( x y : Ordinal ) → x o< omax x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
182 omax-x x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
183 omax-x x y | tri< a ¬b ¬c = ordtrans a <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
184 omax-x x y | tri> ¬a ¬b c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
185 omax-x x y | tri≈ ¬a refl ¬c = <-osuc
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
186
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
187 omax-y : ( x y : Ordinal ) → y o< omax x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
188 omax-y x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
189 omax-y x y | tri< a ¬b ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
190 omax-y x y | tri> ¬a ¬b c = ordtrans c <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
191 omax-y x y | tri≈ ¬a refl ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
192
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
193 omxx : ( x : Ordinal ) → omax x x ≡ osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
194 omxx x with trio< x x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
195 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
196 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
197 omxx x | tri≈ ¬a refl ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
198
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
199 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
200 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
201
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
202 open _∧_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
203
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
204 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
205 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
206 OrdTrans : Transitive _o≤_
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
207 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
208 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
209 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
210 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
211 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc
97
f2b579106770 power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
212
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
213 OrdPreorder : Preorder n n n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
214 OrdPreorder = record { Carrier = Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
215 ; _≈_ = _≡_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
216 ; _∼_ = _o≤_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
217 ; isPreorder = record {
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
218 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
326
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 324
diff changeset
219 ; reflexive = o≤-refl
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
220 ; trans = OrdTrans
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
221 }
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
222 }
165
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
223
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
224 FExists : {m l : Level} → ( ψ : Ordinal → Set m )
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
225 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
226 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
227 → ¬ p
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
228 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
229
393
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
230 nexto∅ : {x : Ordinal} → o∅ o< next x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
231 nexto∅ {x} with trio< o∅ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
232 nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
233 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
234 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
235
339
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
236 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
237 next< {x} {y} {z} x<nz y<nx with trio< y (next z)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
238 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
239 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
240 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
241 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
242 (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
339
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 338
diff changeset
243
342
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 341
diff changeset
244 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 341
diff changeset
245 osuc< {x} {y} refl = <-osuc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 341
diff changeset
246
340
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 339
diff changeset
247 nexto=n : {x y : Ordinal} → x o< next (osuc y) → x o< next y
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
248 nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
340
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 339
diff changeset
249
341
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
250 nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
251 nexto≡ {x} with trio< (next x) (next (osuc x) )
342
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 341
diff changeset
252 -- next x o< next (osuc x ) -> osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
253 nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx x<nx ) a
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
254 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
341
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 340
diff changeset
255 nexto≡ {x} | tri≈ ¬a b ¬c = b
342
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 341
diff changeset
256 -- next (osuc x) o< next x -> osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
348
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
257 nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
08d94fec239c Limit ordinal and possible OD bound
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 347
diff changeset
258 (λ z eq → o<¬≡ (sym eq) (osuc<nx (osuc< (sym eq)))))
346
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 342
diff changeset
259
352
e27769992399 next-is-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 348
diff changeset
260 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
e27769992399 next-is-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 348
diff changeset
261 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
e27769992399 next-is-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 348
diff changeset
262 y<nx : y o< next x
e27769992399 next-is-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 348
diff changeset
263 y<nx = osuc< (sym eq)
e27769992399 next-is-limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 348
diff changeset
264
393
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
265 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
266 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 388
diff changeset
267
309
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
268 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
269 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
270 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
271 os← : Ordinal → Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
272 os←limit : (x : Ordinal) → os← x o< maxordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
273 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
274 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
275
361
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
276 module o≤-Reasoning {n : Level} (O : Ordinals {n} ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
277
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
278 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
280 resp-o< : Ordinals._o<_ O Respects₂ _≡_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
281 resp-o< = resp₂ _o<_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
282
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
283 trans1 : {i j k : Ordinal} → i o< j → j o< osuc k → i o< k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
284 trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
285 trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
286 trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
287
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
288 trans2 : {i j k : Ordinal} → i o< osuc j → j o< k → i o< k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
289 trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
290 trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
291 trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
293 open import Relation.Binary.Reasoning.Base.Triple {n} {_} {_} {_} {Ordinal } {_≡_} {_o≤_} {_o<_}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
294 (Preorder.isPreorder OrdPreorder)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
295 ordtrans --<-trans
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
296 (resp₂ _o<_) --(resp₂ _<_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
297 (λ x → ordtrans x <-osuc ) --<⇒≤
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
298 trans1 --<-transˡ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
299 trans2 --<-transʳ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
300 public
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
301 hiding (_≈⟨_⟩_)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 352
diff changeset
302