annotate Ordinals.agda @ 221:1709c80b7275

fix Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Aug 2019 17:32:21 +0900
parents 95a26d1698f4
children 59771eb07df0
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
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
16
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
18 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set n where
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
19 field
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
20 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
21 OTri : Trichotomous {n} _≡_ _o<_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
22 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
23 <-osuc : { x : ord } → x o< osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
24 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
25
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
26 record Ordinals {n : Level} : Set (suc n) where
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
27 field
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
28 ord : Set n
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
29 o∅ : ord
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
30 osuc : ord → ord
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
31 _o<_ : ord → ord → Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
32 isOrdinal : IsOrdinals ord o∅ osuc _o<_
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
33
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
34 module inOrdinal {n : Level} (O : Ordinals {n} ) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
36 Ordinal : Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
37 Ordinal = Ordinals.ord O
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
38
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
39 _o<_ : Ordinal → Ordinal → Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
40 _o<_ = Ordinals._o<_ O
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
41
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
42 osuc : Ordinal → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
43 osuc = Ordinals.osuc O
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
44
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
45 o∅ : Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
46 o∅ = Ordinals.o∅ O
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
47
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
48 ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
49 osuc-≡< = IsOrdinals.osuc-≡< (Ordinals.isOrdinal O)
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
50 <-osuc = IsOrdinals.<-osuc (Ordinals.isOrdinal 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<-dom : { x y : Ordinal } → x o< y → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
53 o<-dom {x} _ = x
74
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
54
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
55 o<-cod : { x y : Ordinal } → x o< y → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
56 o<-cod {_} {y} _ = y
147
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 144
diff changeset
57
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
58 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
59 o<-subst df refl refl = df
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
60
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
61 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
62 ordtrans = IsOrdinals.Otrans (Ordinals.isOrdinal O)
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
63
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
64 trio< : Trichotomous _≡_ _o<_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
65 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
66
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
67 o<¬≡ : { ox oy : Ordinal } → ox ≡ oy → ox o< oy → ⊥
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
68 o<¬≡ {ox} {oy} eq lt with trio< ox oy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
69 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
70 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
71 o<¬≡ {ox} {oy} eq lt | tri> ¬a ¬b c = ¬b eq
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
72
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
73 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
74 o<> {ox} {oy} lt tl with trio< ox oy
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
75 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
76 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
77 o<> {ox} {oy} lt tl | tri> ¬a ¬b c = ¬a tl
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
78
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
79 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
80 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
81 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
82 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
83
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
84 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
85 ---- y < osuc y < x < osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
86 ---- y < osuc y = x < osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
87 ---- 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
88 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
89 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
90 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
91 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
92 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
93 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
94
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
95 open _∧_
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
96
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
97 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
98 proj2 (osuc2 x y) lt = osucc lt
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
99 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
100 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
101 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
102
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
103 _o≤_ : Ordinal → Ordinal → Set n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
104 a o≤ b = (a ≡ b) ∨ ( a o< b )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
105
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
106
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
107 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
108 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
109 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
110 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
111 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
112
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
113 maxα : Ordinal → Ordinal → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
114 maxα x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
115 maxα x y | tri< a ¬b ¬c = y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
116 maxα x y | tri> ¬a ¬b c = x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
117 maxα x y | tri≈ ¬a refl ¬c = x
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
118
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
119 minα : Ordinal → Ordinal → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
120 minα x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
121 minα x y | tri< a ¬b ¬c = x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
122 minα x y | tri> ¬a ¬b c = y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
123 minα 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
124
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
125 min1 : {x y z : Ordinal } → z o< x → z o< y → z o< minα x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
126 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
127 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
128 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
129 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
130
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
131 --
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
132 -- max ( osuc x , osuc y )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
133 --
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
134
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
135 omax : ( x y : Ordinal ) → Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
136 omax x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
137 omax x y | tri< a ¬b ¬c = osuc y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
138 omax x y | tri> ¬a ¬b c = osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
139 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
140
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
141 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
142 omax< x y lt with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
143 omax< x y lt | tri< a ¬b ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
144 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
145 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
146
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
147 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
148 omax≡ x y eq with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
149 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
150 omax≡ x y eq | tri≈ ¬a refl ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
151 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
152
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
153 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
154 omax-x x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
155 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
156 omax-x x y | tri> ¬a ¬b c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
157 omax-x x y | tri≈ ¬a refl ¬c = <-osuc
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
158
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
159 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
160 omax-y x y with trio< x y
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
161 omax-y x y | tri< a ¬b ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
162 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
163 omax-y x y | tri≈ ¬a refl ¬c = <-osuc
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
164
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
165 omxx : ( x : Ordinal ) → omax x x ≡ osuc x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
166 omxx x with trio< x x
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
167 omxx x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
168 omxx x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
169 omxx x | tri≈ ¬a refl ¬c = refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
170
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
171 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
172 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
173
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
174 open _∧_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
175
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
176 OrdTrans : Transitive _o≤_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
177 OrdTrans (case1 refl) (case1 refl) = case1 refl
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
178 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
179 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
180 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
97
f2b579106770 power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
181
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
182 OrdPreorder : Preorder n n n
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
183 OrdPreorder = record { Carrier = Ordinal
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
184 ; _≈_ = _≡_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
185 ; _∼_ = _o≤_
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
186 ; isPreorder = record {
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
187 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
188 ; reflexive = case1
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
189 ; trans = OrdTrans
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
190 }
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
191 }
165
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
192
221
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
193 TransFiniteExists : {m l : Level} → ( ψ : Ordinal → Set m )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
194 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
195 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
196 → ¬ p
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
197 TransFiniteExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
1709c80b7275 fix Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
198