annotate Ordinals.agda @ 220:95a26d1698f4

try to separate Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Aug 2019 10:28:33 +0900
parents ordinal.agda@eee983e4b402
children 1709c80b7275
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
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
18 record IsOrdinal {n : Level} (Ord : Set n) (_O<_ : Ord → Ord → Set n) : Set n where
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
19 field
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
20 Otrans : {x y z : Ord } → x O< y → y O< z → x O< z
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
21 OTri : Trichotomous {n} _≡_ _O<_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
22
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
23 record Ordinal {n : Level} : Set (suc n) where
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
24 field
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
25 ord : Set n
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
26 O< : ord → ord → Set n
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
27 isOrdinal : IsOrdinal ord O<
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
28
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
29 open Ordinal
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
30
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
31 _o<_ : {n : Level} ( x y : Ordinal {n}) → Set n
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
32 _o<_ x y = O< x {!!} {!!} -- (ord x) (ord y)
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
218
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
34 o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
35 o<-dom {n} {x} _ = x
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
36
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
37 o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
38 o<-cod {n} {_} {y} _ = y
eee983e4b402 try func
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
39
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
40 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
41 o<-subst df refl refl = df
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
42
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
43 o∅ : {n : Level} → Ordinal {n}
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
44 o∅ = {!!}
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
45
74
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
46 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
47 osuc = {!!}
74
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
48
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
49 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
50 <-osuc = {!!}
74
819da8c08f05 ordinal atomical successor?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 73
diff changeset
51
113
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 111
diff changeset
52 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
53 osucc = {!!}
147
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 144
diff changeset
54
203
8edd2a13a7f3 fixing transfinte induction...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 202
diff changeset
55 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
56 o<¬≡ = {!!}
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
57
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
58 ¬x<0 : {n : Level} → { x : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
59 ¬x<0 = {!!}
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 91
diff changeset
60
81
96c932d0145d simpler ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
61 o<> : {n : Level} → {x y : Ordinal {n} } → y o< x → x o< y → ⊥
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
62 o<> = {!!}
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
63
75
714470702a8b Union done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
64 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
65 osuc-≡< = {!!}
75
714470702a8b Union done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
66
714470702a8b Union done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 74
diff changeset
67 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x → x o< y → ⊥
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
68 osuc-< = {!!}
127
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
69
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
70 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
71 a o≤ b = (a ≡ b) ∨ ( a o< b )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
72
27
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
73 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
74 ordtrans = {!!}
27
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
75
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
76 trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
77 trio< = {!!}
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
78
180
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
79 xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa → ox o< ob ) → oa o< osuc ob
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
80 xo<ab {n} {oa} {ob} a→b with trio< oa ob
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
81 xo<ab {n} {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
82 xo<ab {n} {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
83 xo<ab {n} {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) )
11490a3170d4 new ordinal-definable
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 167
diff changeset
84
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
85 maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
86 maxα x y with trio< x y
127
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
87 maxα x y | tri< a ¬b ¬c = y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
88 maxα x y | tri> ¬a ¬b c = x
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
89 maxα x y | tri≈ ¬a refl ¬c = x
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
90
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
91 minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
92 minα {n} x y with trio< {n} x y
127
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
93 minα x y | tri< a ¬b ¬c = x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 113
diff changeset
94 minα x y | tri> ¬a ¬b c = y
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
95 minα x y | tri≈ ¬a refl ¬c = x
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
96
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
97 min1 : {n : Level} → {x y z : Ordinal {n} } → z o< x → z o< y → z o< minα x y
129
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
98 min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
99 min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
100 min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
101 min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
2a5519dcc167 ord power set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
102
85
7494ae6b83c6 omax-induction does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
103 --
7494ae6b83c6 omax-induction does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
104 -- max ( osuc x , osuc y )
7494ae6b83c6 omax-induction does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 84
diff changeset
105 --
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
106
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
107 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
108 omax {n} x y with trio< x y
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
109 omax {n} x y | tri< a ¬b ¬c = osuc y
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
110 omax {n} x y | tri> ¬a ¬b c = osuc x
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
111 omax {n} x y | tri≈ ¬a refl ¬c = osuc x
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
112
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
113 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
114 omax< {n} x y lt with trio< x y
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
115 omax< {n} x y lt | tri< a ¬b ¬c = refl
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
116 omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
117 omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
118
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
119 omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
120 omax≡ {n} x y eq with trio< x y
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
121 omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
122 omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
123 omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
84
4b2aff372b7c omax ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 81
diff changeset
124
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
125 omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
126 omax-x {n} x y with trio< x y
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
127 omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
128 omax-x {n} x y | tri> ¬a ¬b c = <-osuc
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
129 omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
130
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
131 omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
132 omax-y {n} x y with trio< x y
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
133 omax-y {n} x y | tri< a ¬b ¬c = <-osuc
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
134 omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
135 omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
136
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
137 omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
138 omxx {n} x with trio< x x
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
139 omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
140 omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
141 omxx {n} x | tri≈ ¬a refl ¬c = refl
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
142
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
143 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
88
975e72ae0541 osuc work around done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 87
diff changeset
144 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
86
08be6351927e internal error
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 85
diff changeset
145
91
b4742cf4ef97 infinity axiom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
146 open _∧_
b4742cf4ef97 infinity axiom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
147
b4742cf4ef97 infinity axiom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
148 osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
149 osuc2 = {!!}
91
b4742cf4ef97 infinity axiom done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 88
diff changeset
150
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
151 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
152 OrdTrans (case1 refl) (case1 refl) = case1 refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
153 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
154 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
81
96c932d0145d simpler ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
155 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
156
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
157 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
158 OrdPreorder {n} = record { Carrier = Ordinal
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
159 ; _≈_ = _≡_
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
160 ; _∼_ = _o≤_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
161 ; isPreorder = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
162 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
163 ; reflexive = case1
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
164 ; trans = OrdTrans
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
165 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
166 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
167
203
8edd2a13a7f3 fixing transfinte induction...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 202
diff changeset
168 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
169 → {!!}
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
170 → {!!}
22
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
171 → ∀ (x : Ordinal) → ψ x
220
95a26d1698f4 try to separate Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
172 TransFinite {n} {m} {ψ} = {!!}
97
f2b579106770 power set using sup on Def
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
173
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
174 -- we cannot prove this in intutionistic logic
142
c30bc9f5bd0d Power Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 129
diff changeset
175 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
166
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
176 -- postulate
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
177 -- TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
178 -- → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
179 -- → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p )
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
180 -- → p
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
181 --
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
182 -- Instead we prove
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
183 --
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
184 TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
165
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
185 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
186 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
187 → ¬ p
166
ea0e7927637a use double negation
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 165
diff changeset
188 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
165
d16b8bf29f4f minor fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 158
diff changeset
189