|
431
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 open import Level
|
|
|
3 open import Ordinals
|
|
|
4 module ODUtil {n : Level } (O : Ordinals {n} ) where
|
|
|
5
|
|
|
6 open import zf
|
|
|
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
9 open import Data.Nat.Properties
|
|
|
10 open import Data.Empty
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary hiding ( _⇔_ )
|
|
|
13
|
|
|
14 open import logic
|
|
|
15 open import nat
|
|
|
16
|
|
|
17 open Ordinals.Ordinals O
|
|
|
18 open Ordinals.IsOrdinals isOrdinal
|
|
|
19 open Ordinals.IsNext isNext
|
|
|
20 import OrdUtil
|
|
|
21 open OrdUtil O
|
|
|
22
|
|
|
23 import OD
|
|
|
24 open OD O
|
|
|
25 open OD.OD
|
|
|
26 open ODAxiom odAxiom
|
|
|
27
|
|
|
28 open HOD
|
|
|
29 open _∧_
|
|
|
30 open _==_
|
|
|
31
|
|
|
32 cseq : HOD → HOD
|
|
|
33 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
|
|
|
34 lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
|
|
|
35 lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
|
|
|
36
|
|
|
37
|
|
|
38 pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
|
|
|
39 pair-xx<xy {x} {y} = ⊆→o≤ lemma where
|
|
|
40 lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
|
|
|
41 lemma {z} (case1 refl) = case1 refl
|
|
|
42 lemma {z} (case2 refl) = case1 refl
|
|
|
43
|
|
|
44 pair-<xy : {x y : HOD} → {n : Ordinal} → & x o< next n → & y o< next n → & (x , y) o< next n
|
|
|
45 pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
|
|
|
46 ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
|
|
|
47 ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
|
|
|
48 ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
|
|
|
49
|
|
|
50 -- another form of infinite
|
|
|
51 -- pair-ord< : {x : Ordinal } → Set n
|
|
|
52 pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
|
|
|
53 pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where
|
|
|
54 lemmab0 : next (odmax (x , x)) ≡ next (& x)
|
|
|
55 lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
|
|
|
56 lemmab1 : & (x , x) o< next ( odmax (x , x))
|
|
|
57 lemmab1 = ho<
|
|
|
58
|
|
|
59 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
|
|
1096
|
60 trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab)
|
|
431
|
61
|
|
|
62 refl-⊆ : {A : HOD} → A ⊆ A
|
|
1096
|
63 refl-⊆ x = x
|
|
431
|
64
|
|
|
65 od⊆→o≤ : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
|
|
1096
|
66 od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) &iso (lt (d→∋ x x>z)))
|
|
431
|
67
|
|
480
|
68 ⊆→= : {F U : HOD} → F ⊆ U → U ⊆ F → F =h= U
|
|
1096
|
69 ⊆→= {F} {U} FU UF = record { eq→ = λ {x} lt → subst (λ k → odef U k) &iso (FU (subst (λ k → odef F k) (sym &iso) lt) )
|
|
|
70 ; eq← = λ {x} lt → subst (λ k → odef F k) &iso (UF (subst (λ k → odef U k) (sym &iso) lt) ) }
|
|
480
|
71
|
|
519
|
72 ¬A∋x→A≡od∅ : (A : HOD) → {x : HOD} → A ∋ x → ¬ ( & A ≡ o∅ )
|
|
|
73 ¬A∋x→A≡od∅ A {x} ax a=0 = ¬x<0 ( subst (λ k → & x o< k) a=0 (c<→o< ax ))
|
|
|
74
|
|
431
|
75 subset-lemma : {A x : HOD } → ( {y : HOD } → x ∋ y → (A ∩ x ) ∋ y ) ⇔ ( x ⊆ A )
|
|
|
76 subset-lemma {A} {x} = record {
|
|
1096
|
77 proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) ))
|
|
|
78 ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
|
|
431
|
79 }
|
|
|
80
|
|
|
81 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
|
|
|
82 ω<next-o∅ {y} lt = <odmax infinite lt
|
|
|
83
|
|
|
84 nat→ω : Nat → HOD
|
|
|
85 nat→ω Zero = od∅
|
|
|
86 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
|
|
|
87
|
|
|
88 ω→nato : {y : Ordinal} → infinite-d y → Nat
|
|
|
89 ω→nato iφ = Zero
|
|
|
90 ω→nato (isuc lt) = Suc (ω→nato lt)
|
|
|
91
|
|
|
92 ω→nat : (n : HOD) → infinite ∋ n → Nat
|
|
|
93 ω→nat n = ω→nato
|
|
|
94
|
|
|
95 ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
|
|
|
96 ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
|
|
|
97 ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
|
|
|
98 lemma : & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
|
|
|
99 lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
|
|
|
100
|
|
|
101 pair1 : { x y : HOD } → (x , y ) ∋ x
|
|
|
102 pair1 = case1 refl
|
|
|
103
|
|
|
104 pair2 : { x y : HOD } → (x , y ) ∋ y
|
|
|
105 pair2 = case2 refl
|
|
|
106
|
|
|
107 single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
|
|
|
108 single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
|
|
|
109 single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
|
|
|
110
|
|
1096
|
111 single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y
|
|
|
112 single& (case1 eq) = sym (trans eq &iso)
|
|
|
113 single& (case2 eq) = sym (trans eq &iso)
|
|
|
114
|
|
431
|
115 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
|
|
|
116 -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m
|
|
|
117
|
|
1096
|
118 pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c )
|
|
|
119 pair=∨ {a} {b} {c} (case1 c=a) = case1 ( sym (trans c=a &iso))
|
|
|
120 pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso))
|
|
|
121
|
|
431
|
122 ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
|
|
1096
|
123 ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl
|
|
|
124 ; ox = subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y
|
|
|
125 ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u
|
|
|
126 ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin
|
|
|
127 osuc y ≡⟨ sym (cong osuc &iso) ⟩
|
|
|
128 osuc (& (* y)) ≤⟨ osucc (c<→o< {* y} {* u} uy) ⟩ -- * x ≡ * u ∋ * y
|
|
|
129 & (* u) ≡⟨ &iso ⟩
|
|
|
130 u ≡⟨ u=x ⟩
|
|
|
131 & (* x) ≡⟨ &iso ⟩
|
|
|
132 x ∎ ))) where open o≤-Reasoning O
|
|
|
133 ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin
|
|
|
134 x ≡⟨ single& (subst₂ (λ j k → odef j k ) (begin
|
|
|
135 * u ≡⟨ cong (*) u=xx ⟩
|
|
|
136 * (& (* x , * x)) ≡⟨ *iso ⟩
|
|
|
137 (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y
|
|
|
138 y ∎ ) x<y) where open ≡-Reasoning
|
|
431
|
139
|
|
|
140 ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
|
|
|
141 ω-prev-eq {x} {y} eq with trio< x y
|
|
|
142 ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
|
|
|
143 ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
|
|
|
144 ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
|
|
|
145
|
|
|
146 ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x
|
|
1096
|
147 ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) }
|
|
431
|
148
|
|
|
149 ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ )
|
|
|
150 ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
|
|
|
151
|
|
|
152 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
|
|
|
153 nat→ω-iso {i} = ε-induction {λ i → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where
|
|
|
154 ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
|
|
|
155 (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
|
|
|
156 ind {x} prev lt = ind1 lt *iso where
|
|
|
157 ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
|
|
|
158 ind1 {o∅} iφ refl = sym o∅≡od∅
|
|
|
159 ind1 (isuc {x₁} ltd) ox=x = begin
|
|
|
160 nat→ω (ω→nato (isuc ltd) )
|
|
|
161 ≡⟨⟩
|
|
|
162 Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
|
|
|
163 ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩
|
|
|
164 Union (* x₁ , (* x₁ , * x₁))
|
|
|
165 ≡⟨ trans ( sym *iso) ox=x ⟩
|
|
|
166 x
|
|
|
167 ∎ where
|
|
|
168 open ≡-Reasoning
|
|
|
169 lemma0 : x ∋ * x₁
|
|
1096
|
170 lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x)
|
|
|
171 record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl) }
|
|
431
|
172 lemma1 : infinite ∋ * x₁
|
|
|
173 lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
|
|
|
174 lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
|
|
|
175 lemma3 iφ iφ refl = HE.refl
|
|
|
176 lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
|
|
|
177 lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
|
|
|
178 lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
|
|
|
179 ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t
|
|
|
180 lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
|
|
|
181 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where
|
|
|
182 lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
|
|
|
183 lemma6 refl HE.refl = refl
|
|
|
184 lemma : nat→ω (ω→nato ltd) ≡ * x₁
|
|
|
185 lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 )
|
|
|
186
|
|
|
187 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
|
|
|
188 ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
|
|
|
189 lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡ nat→ω i → ω→nato ltd ≡ i
|
|
|
190 lemma {x} Zero iφ eq = refl
|
|
|
191 lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
|
|
|
192 lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅ ) *iso eq ))
|
|
|
193 lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) ) where -- * x ≡ nat→ω i
|
|
|
194 lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
|
|
|
195 lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
|
|
|
196 ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
|
|
|
197 (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
|
|
|
198
|
