comparison OD.agda @ 223:2e1f19c949dc

sepration of ordinal from OD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Aug 2019 17:57:58 +0900
parents 43021d2b8756
children 176ff97547b4
comparison
equal deleted inserted replaced
222:59771eb07df0 223:2e1f19c949dc
1 open import Level 1 open import Level
2 module OD where 2 open import Ordinals
3 module OD {n : Level } (O : Ordinals {n} ) where
3 4
4 open import zf 5 open import zf
5 open import ordinal
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 Relation.Binary.PropositionalEquality 7 open import Relation.Binary.PropositionalEquality
8 open import Data.Nat.Properties 8 open import Data.Nat.Properties
9 open import Data.Empty 9 open import Data.Empty
10 open import Relation.Nullary 10 open import Relation.Nullary
12 open import Relation.Binary.Core 12 open import Relation.Binary.Core
13 13
14 open import logic 14 open import logic
15 open import nat 15 open import nat
16 16
17 open inOrdinal O
18
17 -- Ordinal Definable Set 19 -- Ordinal Definable Set
18 20
19 record OD {n : Level} : Set (suc n) where 21 record OD : Set (suc n ) where
20 field 22 field
21 def : (x : Ordinal {n} ) → Set n 23 def : (x : Ordinal ) → Set n
22 24
23 open OD 25 open OD
24 26
25 open Ordinal
26 open _∧_ 27 open _∧_
27 open _∨_ 28 open _∨_
28 open Bool 29 open Bool
29 30
30 record _==_ {n : Level} ( a b : OD {n} ) : Set n where 31 record _==_ ( a b : OD ) : Set n where
31 field 32 field
32 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x 33 eq→ : ∀ { x : Ordinal } → def a x → def b x
33 eq← : ∀ { x : Ordinal {n} } → def b x → def a x 34 eq← : ∀ { x : Ordinal } → def b x → def a x
34 35
35 id : {n : Level} {A : Set n} → A → A 36 id : {n : Level} {A : Set n} → A → A
36 id x = x 37 id x = x
37 38
38 eq-refl : {n : Level} { x : OD {n} } → x == x 39 eq-refl : { x : OD } → x == x
39 eq-refl {n} {x} = record { eq→ = id ; eq← = id } 40 eq-refl {x} = record { eq→ = id ; eq← = id }
40 41
41 open _==_ 42 open _==_
42 43
43 eq-sym : {n : Level} { x y : OD {n} } → x == y → y == x 44 eq-sym : { x y : OD } → x == y → y == x
44 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } 45 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
45 46
46 eq-trans : {n : Level} { x y z : OD {n} } → x == y → y == z → x == z 47 eq-trans : { x y z : OD } → x == y → y == z → x == z
47 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } 48 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
48 49
49 ⇔→== : {n : Level} { x y : OD {suc n} } → ( {z : Ordinal {suc n}} → def x z ⇔ def y z) → x == y 50 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y
50 eq→ ( ⇔→== {n} {x} {y} eq ) {z} m = proj1 eq m 51 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m
51 eq← ( ⇔→== {n} {x} {y} eq ) {z} m = proj2 eq m 52 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m
52 53
53 -- Ordinal in OD ( and ZFSet ) Transitive Set 54 -- Ordinal in OD ( and ZFSet ) Transitive Set
54 Ord : { n : Level } → ( a : Ordinal {n} ) → OD {n} 55 Ord : ( a : Ordinal ) → OD
55 Ord {n} a = record { def = λ y → y o< a } 56 Ord a = record { def = λ y → y o< a }
56 57
57 od∅ : {n : Level} → OD {n} 58 od∅ : OD
58 od∅ {n} = Ord o∅ 59 od∅ = Ord o∅
59 60
60 postulate 61 postulate
61 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 62 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
62 od→ord : {n : Level} → OD {n} → Ordinal {n} 63 od→ord : OD → Ordinal
63 ord→od : {n : Level} → Ordinal {n} → OD {n} 64 ord→od : Ordinal → OD
64 c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y 65 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y
65 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 66 oiso : {x : OD } → ord→od ( od→ord x ) ≡ x
66 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 67 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
67 -- we should prove this in agda, but simply put here 68 -- we should prove this in agda, but simply put here
68 ==→o≡ : {n : Level} → { x y : OD {suc n} } → (x == y) → x ≡ y 69 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
69 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set 70 -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
70 -- o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x 71 -- o<→c< : {n : Level} {x y : Ordinal } → x o< y → def (ord→od y) x
71 -- ord→od x ≡ Ord x results the same 72 -- ord→od x ≡ Ord x results the same
72 -- supermum as Replacement Axiom 73 -- supermum as Replacement Axiom
73 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 74 sup-o : ( Ordinal → Ordinal ) → Ordinal
74 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 75 sup-o< : { ψ : Ordinal → Ordinal } → ∀ {x : Ordinal } → ψ x o< sup-o ψ
75 -- contra-position of mimimulity of supermum required in Power Set Axiom 76 -- contra-position of mimimulity of supermum required in Power Set Axiom
76 -- sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 77 -- sup-x : {n : Level } → ( Ordinal → Ordinal ) → Ordinal
77 -- sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 78 -- sup-lb : {n : Level } → { ψ : Ordinal → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
78 -- mimimul and x∋minimul is an Axiom of choice 79 -- mimimul and x∋minimul is an Axiom of choice
79 minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 80 minimul : (x : OD ) → ¬ (x == od∅ )→ OD
80 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x ) 81 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
81 x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) ) 82 x∋minimul : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
82 -- minimulity (may proved by ε-induction ) 83 -- minimulity (may proved by ε-induction )
83 minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) ) 84 minimul-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) )
84 85
85 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 86 _∋_ : ( a x : OD ) → Set n
86 _∋_ {n} a x = def a ( od→ord x ) 87 _∋_ a x = def a ( od→ord x )
87 88
88 _c<_ : { n : Level } → ( x a : OD {n} ) → Set n 89 _c<_ : ( x a : OD ) → Set n
89 x c< a = a ∋ x 90 x c< a = a ∋ x
90 91
91 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) 92 _c≤_ : OD → OD → Set (suc n)
92 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 93 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
93 94
94 cseq : {n : Level} → OD {n} → OD {n} 95 cseq : {n : Level} → OD → OD
95 cseq x = record { def = λ y → def x (osuc y) } where 96 cseq x = record { def = λ y → def x (osuc y) } where
96 97
97 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x 98 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x
98 def-subst df refl refl = df 99 def-subst df refl refl = df
99 100
100 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} 101 sup-od : ( OD → OD ) → OD
101 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) 102 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
102 103
103 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x )) 104 sup-c< : ( ψ : OD → OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
104 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )} 105 sup-c< ψ {x} = def-subst {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
105 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where 106 lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
106 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x))) 107 lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
107 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) ) 108 lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso) )
108 109
109 otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y 110 otrans : {n : Level} {a x y : Ordinal } → def (Ord a) x → def (Ord x) y → def (Ord a) y
110 otrans x<a y<x = ordtrans y<x x<a 111 otrans x<a y<x = ordtrans y<x x<a
111 112
112 def→o< : {n : Level } {X : OD {suc n}} → {x : Ordinal {suc n}} → def X x → x o< od→ord X 113 def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X
113 def→o< {n} {X} {x} lt = o<-subst {suc n} {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {suc n} {X} {x} lt (sym oiso) (sym diso) )) diso diso 114 def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso
114
115 ∅3 : {n : Level} → { x : Ordinal {suc n}} → ( ∀(y : Ordinal {suc n}) → ¬ (y o< x ) ) → x ≡ o∅ {suc n}
116 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
117 c0 : Nat → Ordinal {suc n} → Set (suc n)
118 c0 lx x = (∀(y : Ordinal {suc n}) → ¬ (y o< x)) → x ≡ o∅ {suc n}
119 c2 : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → c0 (lv x₁) (record { lv = lv x₁ ; ord = ord x₁ }))→ c0 lx (record { lv = lx ; ord = Φ lx } )
120 c2 Zero _ not = refl
121 c2 (Suc lx) _ not with not ( record { lv = lx ; ord = Φ lx } )
122 ... | t with t (case1 ≤-refl )
123 c2 (Suc lx) _ not | t | ()
124 c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx (record { lv = lx ; ord = x₁ }) → c0 lx (record { lv = lx ; ord = OSuc lx x₁ })
125 c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } )
126 ... | t with t (case2 Φ< )
127 c3 lx (Φ .lx) d not | t | ()
128 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } )
129 ... | t with t (case2 (s< s<refl ) )
130 c3 lx (OSuc .lx x₁) d not | t | ()
131
132 ∅5 : {n : Level} → { x : Ordinal {n} } → ¬ ( x ≡ o∅ {n} ) → o∅ {n} o< x
133 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl)
134 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
135 ∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n)
136
137 ord-iso : {n : Level} {y : Ordinal {n} } → record { lv = lv (od→ord (ord→od y)) ; ord = ord (od→ord (ord→od y)) } ≡ record { lv = lv y ; ord = ord y }
138 ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
139 115
140 -- avoiding lv != Zero error 116 -- avoiding lv != Zero error
141 orefl : {n : Level} → { x : OD {n} } → { y : Ordinal {n} } → od→ord x ≡ y → od→ord x ≡ y 117 orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y
142 orefl refl = refl 118 orefl refl = refl
143 119
144 ==-iso : {n : Level} → { x y : OD {n} } → ord→od (od→ord x) == ord→od (od→ord y) → x == y 120 ==-iso : { x y : OD } → ord→od (od→ord x) == ord→od (od→ord y) → x == y
145 ==-iso {n} {x} {y} eq = record { 121 ==-iso {x} {y} eq = record {
146 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ; 122 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ;
147 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) } 123 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) }
148 where 124 where
149 lemma : {x : OD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z 125 lemma : {x : OD } {z : Ordinal } → def (ord→od (od→ord x)) z → def x z
150 lemma {x} {z} d = def-subst d oiso refl 126 lemma {x} {z} d = def-subst d oiso refl
151 127
152 =-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y) 128 =-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) == y)
153 =-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso) 129 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso)
154 130
155 ord→== : {n : Level} → { x y : OD {n} } → od→ord x ≡ od→ord y → x == y 131 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y
156 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where 132 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
157 lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy → (ord→od ox) == (ord→od oy) 133 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (ord→od ox) == (ord→od oy)
158 lemma ox ox refl = eq-refl 134 lemma ox ox refl = eq-refl
159 135
160 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y 136 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x == ord→od y
161 o≡→== {n} {x} {.x} refl = eq-refl 137 o≡→== {x} {.x} refl = eq-refl
162 138
163 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x 139 c≤-refl : {n : Level} → ( x : OD ) → x c≤ x
164 c≤-refl x = case1 refl 140 c≤-refl x = case1 refl
165 141
166 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 142 o∅≡od∅ : ord→od (o∅ ) ≡ od∅
167 o∅≡od∅ {n} = ==→o≡ lemma where 143 o∅≡od∅ = ==→o≡ lemma where
168 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x 144 lemma0 : {x : Ordinal} → def (ord→od o∅) x → def od∅ x
169 lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso 145 lemma0 {x} lt = o<-subst (c<→o< {ord→od x} {ord→od o∅} (def-subst {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
170 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x 146 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅) x
171 lemma1 (case1 ()) 147 lemma1 {x} lt = ⊥-elim (¬x<0 lt)
172 lemma1 (case2 ())
173 lemma : ord→od o∅ == od∅ 148 lemma : ord→od o∅ == od∅
174 lemma = record { eq→ = lemma0 ; eq← = lemma1 } 149 lemma = record { eq→ = lemma0 ; eq← = lemma1 }
175 150
176 ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n} 151 ord-od∅ : od→ord (od∅ ) ≡ o∅
177 ord-od∅ {n} = sym ( subst (λ k → k ≡ od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) ) 152 ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
178 153
179 ∅0 : {n : Level} → record { def = λ x → Lift n ⊥ } == od∅ {n} 154 ∅0 : record { def = λ x → Lift n ⊥ } == od∅
180 eq→ ∅0 {w} (lift ()) 155 eq→ ∅0 {w} (lift ())
181 eq← ∅0 {w} (case1 ()) 156 eq← ∅0 {w} lt = lift (¬x<0 lt)
182 eq← ∅0 {w} (case2 ()) 157
183 158 ∅< : { x y : OD } → def x (od→ord y ) → ¬ ( x == od∅ )
184 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} ) 159 ∅< {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
185 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d 160 ∅< {x} {y} d eq | lift ()
186 ∅< {n} {x} {y} d eq | lift ()
187 161
188 ∅6 : {n : Level} → { x : OD {suc n} } → ¬ ( x ∋ x ) -- no Russel paradox 162 ∅6 : { x : OD } → ¬ ( x ∋ x ) -- no Russel paradox
189 ∅6 {n} {x} x∋x = o<¬≡ refl ( c<→o< {suc n} {x} {x} x∋x ) 163 ∅6 {x} x∋x = o<¬≡ refl ( c<→o< {x} {x} x∋x )
190 164
191 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y → (def A y → def B y) → def A x → def B x 165 def-iso : {A B : OD } {x y : Ordinal } → x ≡ y → (def A y → def B y) → def A x → def B x
192 def-iso refl t = t 166 def-iso refl t = t
193 167
194 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) 168 is-o∅ : ( x : Ordinal ) → Dec ( x ≡ o∅ )
195 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl 169 is-o∅ x with trio< x o∅
196 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) 170 is-o∅ x | tri< a ¬b ¬c = no ¬b
197 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) 171 is-o∅ x | tri≈ ¬a b ¬c = yes b
198 172 is-o∅ x | tri> ¬a ¬b c = no ¬b
199 ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p 173
200 ppp {n} {p} {a} d = d 174 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
175 ppp {p} {a} d = d
201 176
202 -- 177 --
203 -- Axiom of choice in intutionistic logic implies the exclude middle 178 -- Axiom of choice in intutionistic logic implies the exclude middle
204 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog 179 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
205 -- 180 --
206 p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p ) -- assuming axiom of choice 181 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
207 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } )) 182 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } ))
208 p∨¬p {n} p | yes eq = case2 (¬p eq) where 183 p∨¬p p | yes eq = case2 (¬p eq) where
209 ps = record { def = λ x → p } 184 ps = record { def = λ x → p }
210 lemma : ps == od∅ → p → ⊥ 185 lemma : ps == od∅ → p → ⊥
211 lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 ) 186 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
212 ¬p : (od→ord ps ≡ o∅) → p → ⊥ 187 ¬p : (od→ord ps ≡ o∅) → p → ⊥
213 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq )) 188 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
214 p∨¬p {n} p | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where 189 p∨¬p p | no ¬p = case1 (ppp {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} lemma) where
215 ps = record { def = λ x → p } 190 ps = record { def = λ x → p }
216 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} 191 eqo∅ : ps == od∅ → od→ord ps ≡ o∅
217 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 192 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
218 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) 193 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq))
219 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) 194 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq))
220 195
221 ∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p -- assuming axiom of choice 196 ∋-p : ( p : Set n ) → Dec p -- assuming axiom of choice
222 ∋-p {n} p with p∨¬p p 197 ∋-p p with p∨¬p p
223 ∋-p {n} p | case1 x = yes x 198 ∋-p p | case1 x = yes x
224 ∋-p {n} p | case2 x = no x 199 ∋-p p | case2 x = no x
225 200
226 double-neg-eilm : {n : Level } {A : Set (suc n)} → ¬ ¬ A → A -- we don't have this in intutionistic logic 201 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
227 double-neg-eilm {n} {A} notnot with ∋-p A -- assuming axiom of choice 202 double-neg-eilm {A} notnot with ∋-p A -- assuming axiom of choice
228 ... | yes p = p 203 ... | yes p = p
229 ... | no ¬p = ⊥-elim ( notnot ¬p ) 204 ... | no ¬p = ⊥-elim ( notnot ¬p )
230 205
231 OrdP : {n : Level} → ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y ) 206 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y )
232 OrdP {n} x y with trio< x (od→ord y) 207 OrdP x y with trio< x (od→ord y)
233 OrdP {n} x y | tri< a ¬b ¬c = no ¬c 208 OrdP x y | tri< a ¬b ¬c = no ¬c
234 OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) 209 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
235 OrdP {n} x y | tri> ¬a ¬b c = yes c 210 OrdP x y | tri> ¬a ¬b c = yes c
236 211
237 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 212 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
238 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) 213 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
239 214
240 in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n} 215 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD
241 in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) } 216 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y ))))) }
242 217
243 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 218 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
244 219
245 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} 220 ZFSubset : (A x : OD ) → OD
246 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set 221 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set
247 222
248 Def : {n : Level} → (A : OD {suc n}) → OD {suc n} 223 Def : (A : OD ) → OD
249 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 224 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
250 225
251 226
252 _⊆_ : {n : Level} ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n) 227 _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n
253 _⊆_ A B {x} = A ∋ x → B ∋ x 228 _⊆_ A B {x} = A ∋ x → B ∋ x
254 229
255 infixr 220 _⊆_ 230 infixr 220 _⊆_
256 231
257 subset-lemma : {n : Level} → {A x y : OD {suc n} } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) 232 subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} )
258 subset-lemma {n} {A} {x} {y} = record { 233 subset-lemma {A} {x} {y} = record {
259 proj1 = λ z lt → proj1 (z lt) 234 proj1 = λ z lt → proj1 (z lt)
260 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } 235 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
261 } 236 }
262 237
263 -- Constructible Set on α 238 -- Constructible Set on α
264 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x } 239 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y < od→ord x }
265 -- L (Φ 0) = Φ 240 -- L (Φ 0) = Φ
266 -- L (OSuc lv n) = { Def ( L n ) } 241 -- L (OSuc lv n) = { Def ( L n ) }
267 -- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) ) 242 -- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) )
268 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n} 243 -- L : {n : Level} → (α : Ordinal ) → OD
269 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ 244 -- L record { lv = Zero ; ord = (Φ .0) } = od∅
270 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 245 -- L record { lv = lx ; ord = (OSuc lv ox) } = Def ( L ( record { lv = lx ; ord = ox } ) )
271 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) 246 -- L record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
272 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) 247 -- cseq ( Ord (od→ord (L (record { lv = lx ; ord = Φ lx }))))
273 248
274 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α 249 -- L0 : {n : Level} → (α : Ordinal ) → L (osuc α) ∋ L α
275 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x 250 -- L1 : {n : Level} → (α β : Ordinal ) → α o< β → ∀ (x : OD ) → L α ∋ x → L β ∋ x
276 251
277 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 252 OD→ZF : ZF
278 OD→ZF {n} = record { 253 OD→ZF = record {
279 ZFSet = OD {suc n} 254 ZFSet = OD
280 ; _∋_ = _∋_ 255 ; _∋_ = _∋_
281 ; _≈_ = _==_ 256 ; _≈_ = _==_
282 ; ∅ = od∅ 257 ; ∅ = od∅
283 ; _,_ = _,_ 258 ; _,_ = _,_
284 ; Union = Union 259 ; Union = Union
286 ; Select = Select 261 ; Select = Select
287 ; Replace = Replace 262 ; Replace = Replace
288 ; infinite = infinite 263 ; infinite = infinite
289 ; isZF = isZF 264 ; isZF = isZF
290 } where 265 } where
291 ZFSet = OD {suc n} 266 ZFSet = OD
292 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n} 267 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
293 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 268 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
294 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} 269 Replace : OD → (OD → OD ) → OD
295 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 270 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
296 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 271 _,_ : OD → OD → OD
297 x , y = Ord (omax (od→ord x) (od→ord y)) 272 x , y = Ord (omax (od→ord x) (od→ord y))
298 _∩_ : ( A B : ZFSet ) → ZFSet 273 _∩_ : ( A B : ZFSet ) → ZFSet
299 A ∩ B = record { def = λ x → def A x ∧ def B x } 274 A ∩ B = record { def = λ x → def A x ∧ def B x }
300 Union : OD {suc n} → OD {suc n} 275 Union : OD → OD
301 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 276 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
302 _∈_ : ( A B : ZFSet ) → Set (suc n) 277 _∈_ : ( A B : ZFSet ) → Set n
303 A ∈ B = B ∋ A 278 A ∈ B = B ∋ A
304 Power : OD {suc n} → OD {suc n} 279 Power : OD → OD
305 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 280 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
306 {_} : ZFSet → ZFSet 281 {_} : ZFSet → ZFSet
307 { x } = ( x , x ) 282 { x } = ( x , x )
308 283
309 data infinite-d : ( x : Ordinal {suc n} ) → Set (suc n) where 284 data infinite-d : ( x : Ordinal ) → Set n where
310 iφ : infinite-d o∅ 285 iφ : infinite-d o∅
311 isuc : {x : Ordinal {suc n} } → infinite-d x → 286 isuc : {x : Ordinal } → infinite-d x →
312 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) 287 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
313 288
314 infinite : OD {suc n} 289 infinite : OD
315 infinite = record { def = λ x → infinite-d x } 290 infinite = record { def = λ x → infinite-d x }
316 291
317 infixr 200 _∈_ 292 infixr 200 _∈_
318 -- infixr 230 _∩_ _∪_ 293 -- infixr 230 _∩_ _∪_
319 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite 294 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite
320 isZF = record { 295 isZF = record {
321 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 296 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
322 ; pair = pair 297 ; pair = pair
323 ; union→ = union→ 298 ; union→ = union→
324 ; union← = union← 299 ; union← = union←
325 ; empty = empty 300 ; empty = empty
326 ; power→ = power→ 301 ; power→ = power→
327 ; power← = power← 302 ; power← = power←
328 ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 303 ; extensionality = λ {A} {B} {w} → extensionality {A} {B} {w}
329 ; ε-induction = ε-induction 304 -- ; ε-induction = {!!}
330 ; infinity∅ = infinity∅ 305 ; infinity∅ = infinity∅
331 ; infinity = infinity 306 ; infinity = infinity
332 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} 307 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
333 ; replacement← = replacement← 308 ; replacement← = replacement←
334 ; replacement→ = replacement→ 309 ; replacement→ = replacement→
335 ; choice-func = choice-func 310 ; choice-func = choice-func
336 ; choice = choice 311 ; choice = choice
337 } where 312 } where
338 313
339 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 314 pair : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
340 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 315 proj1 (pair A B ) = omax-x (od→ord A) (od→ord B)
341 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 316 proj2 (pair A B ) = omax-y (od→ord A) (od→ord B)
342 317
343 empty : {n : Level } (x : OD {suc n} ) → ¬ (od∅ ∋ x) 318 empty : (x : OD ) → ¬ (od∅ ∋ x)
344 empty x (case1 ()) 319 empty x = ¬x<0
345 empty x (case2 ()) 320
346 321 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z}
347 o<→c< : {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_ (Ord x) (Ord y) {z}
348 o<→c< lt lt1 = ordtrans lt1 lt 322 o<→c< lt lt1 = ordtrans lt1 lt
349 323
350 ⊆→o< : {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y 324 ⊆→o< : {x y : Ordinal } → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y
351 ⊆→o< {x} {y} lt with trio< x y 325 ⊆→o< {x} {y} lt with trio< x y
352 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc 326 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc
353 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc 327 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
354 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) 328 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
355 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) 329 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
360 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) 334 union← : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z )))
361 union← X z UX∋z = TransFiniteExists _ lemma UX∋z where 335 union← X z UX∋z = TransFiniteExists _ lemma UX∋z where
362 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z)) 336 lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
363 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 337 lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
364 338
365 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 339 ψiso : {ψ : OD → Set n} {x y : OD } → ψ x → x ≡ y → ψ y
366 ψiso {ψ} t refl = t 340 ψiso {ψ} t refl = t
367 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 341 selection : {ψ : OD → Set n} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
368 selection {ψ} {X} {y} = record { 342 selection {ψ} {X} {y} = record {
369 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 343 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }
370 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } 344 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso }
371 } 345 }
372 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x 346 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x
390 --- 364 ---
391 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A 365 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y } subset of A
392 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A 366 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) Power X is a sup of all subset of A
393 -- 367 --
394 -- 368 --
395 ∩-≡ : { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a ) 369 ∩-≡ : { a b : OD } → ({x : OD } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
396 ∩-≡ {a} {b} inc = record { 370 ∩-≡ {a} {b} inc = record {
397 eq→ = λ {x} x<a → record { proj2 = x<a ; 371 eq→ = λ {x} x<a → record { proj2 = x<a ;
398 proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; 372 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ;
399 eq← = λ {x} x<a∩b → proj2 x<a∩b } 373 eq← = λ {x} x<a∩b → proj2 x<a∩b }
400 -- 374 --
401 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 375 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
402 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 376 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
403 -- 377 --
404 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t 378 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
405 ord-power← a t t→A = def-subst {suc n} {_} {_} {Def (Ord a)} {od→ord t} 379 ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t}
406 lemma refl (lemma1 lemma-eq )where 380 lemma refl (lemma1 lemma-eq )where
407 lemma-eq : ZFSubset (Ord a) t == t 381 lemma-eq : ZFSubset (Ord a) t == t
408 eq→ lemma-eq {z} w = proj2 w 382 eq→ lemma-eq {z} w = proj2 w
409 eq← lemma-eq {z} w = record { proj2 = w ; 383 eq← lemma-eq {z} w = record { proj2 = w ;
410 proj1 = def-subst {suc n} {_} {_} {(Ord a)} {z} 384 proj1 = def-subst {_} {_} {(Ord a)} {z}
411 ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 385 ( t→A (def-subst {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
412 lemma1 : {n : Level } {a : Ordinal {suc n}} { t : OD {suc n}} 386 lemma1 : {a : Ordinal } { t : OD }
413 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 387 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
414 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) 388 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
415 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) 389 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
416 lemma = sup-o< 390 lemma = sup-o<
417 391
418 -- 392 --
419 -- Every set in OD is a subset of Ordinals 393 -- Every set in OD is a subset of Ordinals
440 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x 414 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
441 lemma0 {x} t∋x = c<→o< (t→A t∋x) 415 lemma0 {x} t∋x = c<→o< (t→A t∋x)
442 lemma3 : Def (Ord a) ∋ t 416 lemma3 : Def (Ord a) ∋ t
443 lemma3 = ord-power← a t lemma0 417 lemma3 = ord-power← a t lemma0
444 lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x)) 418 lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x))
445 lt1 = sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} 419 lt1 = sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
446 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t 420 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t
447 lemma4 = let open ≡-Reasoning in begin 421 lemma4 = let open ≡-Reasoning in begin
448 A ∩ ord→od (od→ord t) 422 A ∩ ord→od (od→ord t)
449 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ 423 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
450 A ∩ t 424 A ∩ t
451 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 425 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
452 t 426 t
453 427
454 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) 428 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
455 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) 429 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x)))
456 lemma4 (sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}) 430 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t})
457 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) 431 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
458 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 432 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
459 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 433 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
460 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) 434 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))
461 435
465 proj1 (regularity x not ) = x∋minimul x not 439 proj1 (regularity x not ) = x∋minimul x not
466 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where 440 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
467 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁ 441 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
468 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where 442 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where
469 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁)) 443 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
470 lemma3 = record { proj1 = def-subst {suc n} {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso) 444 lemma3 = record { proj1 = def-subst {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso)
471 ; proj2 = proj2 (proj2 s) } 445 ; proj2 = proj2 (proj2 s) }
472 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ 446 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
473 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) )) 447 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
474 448
475 extensionality0 : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 449 extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
476 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 450 eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
477 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 451 eq← (extensionality0 {A} {B} eq ) {x} d = def-iso {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
478 452
479 extensionality : {A B w : OD {suc n} } → ((z : OD {suc n}) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B) 453 extensionality : {A B w : OD } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
480 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d 454 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
481 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 455 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
482 456
483 infinity∅ : infinite ∋ od∅ {suc n} 457 infinity∅ : infinite ∋ od∅
484 infinity∅ = def-subst {suc n} {_} {_} {infinite} {od→ord (od∅ {suc n})} iφ refl lemma where 458 infinity∅ = def-subst {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
485 lemma : o∅ ≡ od→ord od∅ 459 lemma : o∅ ≡ od→ord od∅
486 lemma = let open ≡-Reasoning in begin 460 lemma = let open ≡-Reasoning in begin
487 o∅ 461 o∅
488 ≡⟨ sym diso ⟩ 462 ≡⟨ sym diso ⟩
489 od→ord ( ord→od o∅ ) 463 od→ord ( ord→od o∅ )
490 ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩ 464 ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
491 od→ord od∅ 465 od→ord od∅
492 466
493 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) 467 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
494 infinity x lt = def-subst {suc n} {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where 468 infinity x lt = def-subst {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
495 lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x)))) 469 lemma : od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
496 ≡ od→ord (Union (x , (x , x))) 470 ≡ od→ord (Union (x , (x , x)))
497 lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 471 lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso
498 472
499 -- Axiom of choice ( is equivalent to the existence of minimul in our case ) 473 -- Axiom of choice ( is equivalent to the existence of minimul in our case )
500 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 474 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
501 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD 475 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
502 choice-func X {x} not X∋x = minimul x not 476 choice-func X {x} not X∋x = minimul x not
503 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 477 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
504 choice X {A} X∋A not = x∋minimul A not 478 choice X {A} X∋A not = x∋minimul A not
505 479
506 --
507 -- another form of regularity
508 --
509 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
510 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x )
511 → (x : OD {suc n} ) → ψ x
512 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where
513 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
514 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
515 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x =
516 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
517 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
518 lemma z lt with osuc-≡< y<x
519 lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
520 lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1
521 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =
522 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where
523 --
524 -- if lv of z if less than x Ok
525 -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma
526 --
527 -- lx Suc lx (1) lz(a) <lx by case1
528 -- ly(1) ly(2) (2) lz(b) <lx by case1
529 -- lz(a) lz(b) lz(c) lz(c) <lx by case2 ( ly==lz==lx)
530 --
531 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥
532 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2
533 lemma1 : {n : Level } {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly
534 lemma1 {n} {ly} {oy} = let open ≡-Reasoning in begin
535 lv (od→ord (ord→od (record { lv = ly ; ord = oy })))
536 ≡⟨ cong ( λ k → lv k ) diso ⟩
537 lv (record { lv = ly ; ord = oy })
538 ≡⟨⟩
539 ly
540
541 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
542 lemma z lt with c<→o< {suc n} {z} {ord→od (record { lv = ly ; ord = oy })} lt
543 lemma z lt | case1 lz<ly with <-cmp lx ly
544 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
545 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1)
546 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
547 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a)
548 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
549 lemma z lt | case2 lz=ly with <-cmp lx ly
550 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
551 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b)
552 ... | eq = subst (λ k → ψ k ) oiso
553 (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
554 lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c)
555 ... | eq = lemma6 {ly} {Φ lx} {oy} lx=ly (sym (subst (λ k → lv (od→ord z) ≡ k) lemma1 eq)) where
556 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z
557 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt )
558 lemma6 : { ly : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } →
559 lx ≡ ly → ly ≡ lv (od→ord z) → ψ z
560 lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
561
562 ---
563 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
564 ---
565 record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
566 field
567 a-choice : OD {suc n}
568 is-in : X ∋ a-choice
569 choice-func' : (X : OD {suc n} ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
570 choice-func' X p∨¬p not = have_to_find
571 where
572 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
573 ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X
574 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
575 lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc ox where
576 ∋-p' : (A x : OD {suc n} ) → Dec ( A ∋ x )
577 ∋-p' A x with p∨¬p ( A ∋ x )
578 ∋-p' A x | case1 t = yes t
579 ∋-p' A x | case2 t = no t
580 ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
581 → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B
582 ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x)
583 ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
584 ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
585 lemma : ¬ ((x : Ordinal {suc n}) → A x) → B
586 lemma not with p∨¬p B
587 lemma not | case1 b = b
588 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
589 caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
590 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
591 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
592 caseΦ lx prev | no ¬p = lemma where
593 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
594 lemma1 x with trio< x (ordinal lx (Φ lx))
595 lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
596 lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx)
597 lemma2 (case1 lt) = case1 lt
598 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
599 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
600 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
601 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
602 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
603 lemma = ∀-imply-or lemma1
604 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
605 caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
606 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
607 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
608 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
609 lemma y lt with trio< y (ordinal lx x )
610 lemma y lt | tri< a ¬b ¬c = not_found y a
611 lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
612 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
613 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
614 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
615 caseOSuc lx x (case2 found) | no ¬p = case2 found
616 have_to_find : choiced X
617 have_to_find with lemma-ord (od→ord X )
618 have_to_find | t = dont-or t ¬¬X∋x where
619 ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
620 ¬¬X∋x nn = not record {
621 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
622 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
623 }
624