|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
433
|
3 module PFOD {n : Level } (O : Ordinals {n}) where
|
|
431
|
4
|
|
|
5 import filter
|
|
|
6 open import logic
|
|
|
7 -- open import partfunc {n} O
|
|
|
8 import OD
|
|
|
9
|
|
|
10 open import Relation.Nullary
|
|
|
11 open import Relation.Binary
|
|
|
12 open import Data.Empty
|
|
|
13 open import Relation.Binary
|
|
|
14 open import Relation.Binary.Core
|
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
|
16 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
1124
|
17 import BAlgebra
|
|
431
|
18
|
|
1124
|
19 open BAlgebra O
|
|
431
|
20
|
|
|
21 open inOrdinal O
|
|
|
22 open OD O
|
|
|
23 open OD.OD
|
|
|
24 open ODAxiom odAxiom
|
|
1297
|
25 -- open ODAxiom-ho< odAxiom-ho<
|
|
431
|
26 import OrdUtil
|
|
|
27 import ODUtil
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
1300
|
30 -- open Ordinals.IsNext isNext
|
|
431
|
31 open OrdUtil O
|
|
|
32 open ODUtil O
|
|
|
33
|
|
|
34
|
|
|
35 import ODC
|
|
|
36
|
|
|
37 open filter O
|
|
|
38
|
|
|
39 open _∧_
|
|
|
40 open _∨_
|
|
|
41 open Bool
|
|
|
42
|
|
|
43
|
|
|
44 open HOD
|
|
|
45
|
|
|
46 -------
|
|
|
47 -- the set of finite partial functions from ω to 2
|
|
|
48 --
|
|
|
49 --
|
|
|
50
|
|
|
51 open import Data.List hiding (filter)
|
|
|
52 open import Data.Maybe
|
|
|
53
|
|
1218
|
54 open import ZProduct O
|
|
431
|
55
|
|
|
56 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
|
|
|
57 hφ : Hω2 0 o∅
|
|
|
58 h0 : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
1301
|
59 Hω2 (Suc i) (& (Union (< nat→ω i , od∅ > , * x )))
|
|
|
60 h1 : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
|
61 Hω2 (Suc i) (& (Union (< nat→ω i , nat→ω 1 > , * x )))
|
|
431
|
62 he : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
|
63 Hω2 (Suc i) x
|
|
|
64
|
|
|
65 record Hω2r (x : Ordinal) : Set n where
|
|
|
66 field
|
|
|
67 count : Nat
|
|
|
68 hω2 : Hω2 count x
|
|
|
69
|
|
|
70 open Hω2r
|
|
|
71
|
|
1301
|
72 hw⊆POmega : {x : Ordinal} → Hω2r x → odef (Power (Power Omega )) x
|
|
|
73 hw⊆POmega {x} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where
|
|
|
74 odmax1 : {y : Ordinal} (i : Nat) → Hω2 i y → odef (Power (Power Omega )) y
|
|
1300
|
75 odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz ))
|
|
|
76 odmax1 (Suc i) (h0 {_} {y} hw) = pf01 where
|
|
1301
|
77 pf00 : odef ( Power (Power Omega)) y
|
|
1300
|
78 pf00 = odmax1 i hw
|
|
1301
|
79 pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 0 > , * y)))
|
|
1300
|
80 pf01 z xz with subst (λ k → odef k z ) *iso xz
|
|
|
81 ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
|
|
1301
|
82 pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
|
|
|
83 pf02 w zw with subst (λ k → odef k z) *iso ox
|
|
|
84 ... | case2 refl with subst (λ k → odef k w) *iso zw
|
|
|
85 ... | case1 refl = ω∋nat→ω {i}
|
|
|
86 ... | case2 refl = ω∋nat→ω {0}
|
|
|
87 pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
|
|
|
88 ... | case1 refl = ω∋nat→ω {i}
|
|
|
89 ... | case2 refl = ω∋nat→ω {i}
|
|
|
90 ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
|
|
|
91 pf03 : odef ( Power (Power Omega)) y
|
|
|
92 pf03 = odmax1 i hw
|
|
|
93 pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
|
|
|
94 pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox) _ zw
|
|
|
95 odmax1 (Suc i) (h1 {_} {y} hw) = pf01 where
|
|
|
96 pf00 : odef ( Power (Power Omega)) y
|
|
|
97 pf00 = odmax1 i hw
|
|
|
98 pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 1 > , * y)))
|
|
|
99 pf01 z xz with subst (λ k → odef k z ) *iso xz
|
|
|
100 ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
|
|
|
101 pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
|
|
|
102 pf02 w zw with subst (λ k → odef k z) *iso ox
|
|
|
103 ... | case2 refl with subst (λ k → odef k w) *iso zw
|
|
|
104 ... | case1 refl = ω∋nat→ω {i}
|
|
|
105 ... | case2 refl = ω∋nat→ω {1}
|
|
|
106 pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw
|
|
1300
|
107 ... | case1 refl = ω∋nat→ω {i}
|
|
|
108 ... | case2 refl = ω∋nat→ω {i}
|
|
1301
|
109 ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where
|
|
|
110 pf03 : odef ( Power (Power Omega)) y
|
|
|
111 pf03 = odmax1 i hw
|
|
|
112 pf02 : (w : Ordinal) → odef (* z) w → Omega-d w
|
|
|
113 pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox) _ zw
|
|
1300
|
114 odmax1 (Suc i) (he {_} {y} hw) = pf00 where
|
|
1301
|
115 pf00 : odef ( Power (Power Omega)) y
|
|
1300
|
116 pf00 = odmax1 i hw
|
|
|
117
|
|
|
118 --
|
|
|
119 -- Set of limited partial function of Omega
|
|
|
120 --
|
|
431
|
121 HODω2 : HOD
|
|
1301
|
122 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power (Power Omega))
|
|
1300
|
123 ; <odmax = λ lt → odef< (hw⊆POmega lt) }
|
|
|
124
|
|
1301
|
125 HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Power Omega
|
|
1300
|
126 HODω2⊆Omega {x} hx {z} wz = hw⊆POmega hx _ (subst (λ k → odef k z) (sym *iso) wz)
|
|
|
127
|
|
|
128 record HwStep : Set n where
|
|
|
129 field
|
|
|
130 x : Ordinal
|
|
|
131 i : Nat
|
|
|
132 isHw : Hω2 i x
|
|
431
|
133
|
|
1301
|
134 3→Hω2 : List (Maybe Two) → HOD
|
|
1300
|
135 3→Hω2 t = * (HwStep.x (list→hod t)) where
|
|
1301
|
136 list→hod : List (Maybe Two) → HwStep
|
|
1300
|
137 list→hod [] = record { x = o∅ ; i = 0 ; isHw = hφ }
|
|
1301
|
138 list→hod (just i0 ∷ t) = record { x = & (Union ( < nat→ω (HwStep.i pf01) , od∅ > , * x ))
|
|
1300
|
139 ; i = Suc (HwStep.i pf01) ; isHw = h0 (HwStep.isHw pf01) } where
|
|
|
140 pf01 : HwStep
|
|
|
141 pf01 = list→hod t
|
|
|
142 x = HwStep.x pf01
|
|
1301
|
143 list→hod (just i1 ∷ t) = record { x = & (Union ( < nat→ω (HwStep.i pf01) , nat→ω 1 > , * x ))
|
|
|
144 ; i = Suc (HwStep.i pf01) ; isHw = h1 (HwStep.isHw pf01) } where
|
|
|
145 pf01 : HwStep
|
|
|
146 pf01 = list→hod t
|
|
|
147 x = HwStep.x pf01
|
|
|
148 list→hod (nothing ∷ t) = list→hod t
|
|
431
|
149
|
|
1301
|
150 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two)
|
|
431
|
151 Hω2→3 x = lemma where
|
|
1301
|
152 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two)
|
|
431
|
153 lemma record { count = 0 ; hω2 = hφ } = []
|
|
1301
|
154 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 }
|
|
|
155 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 }
|
|
|
156 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 }
|
|
431
|
157
|
|
|
158 ω→2 : HOD
|
|
1300
|
159 ω→2 = Power Omega
|
|
431
|
160
|
|
1099
|
161 ω2→f : (x : HOD) → ω→2 ∋ x → Nat → Two
|
|
|
162 ω2→f x lt n with ODC.∋-p O x (nat→ω n)
|
|
|
163 ω2→f x lt n | yes p = i1
|
|
|
164 ω2→f x lt n | no ¬p = i0
|
|
431
|
165
|
|
|
166 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
|
|
1300
|
167 fω→2-sel f x = (Omega ∋ x) ∧ ( (lt : odef Omega (& x) ) → f (ω→nat x lt) ≡ i1 )
|
|
431
|
168
|
|
|
169 fω→2 : (Nat → Two) → HOD
|
|
1300
|
170 fω→2 f = Select Omega (fω→2-sel f)
|
|
431
|
171
|
|
|
172 open _==_
|
|
|
173
|
|
|
174 import Axiom.Extensionality.Propositional
|
|
|
175 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
|
|
|
176
|
|
|
177 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
|
|
1300
|
178 ω2∋f f = power← Omega (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {Omega} )) lt))
|
|
431
|
179
|
|
1300
|
180 ω→2f≡i1 : (X i : HOD) → (iω : Omega ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω) ≡ i1 → X ∋ i
|
|
431
|
181 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
|
|
|
182 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
|
|
|
183
|
|
1099
|
184 ω2→f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω2→f X lt ) =h= X
|
|
|
185 eq→ (ω2→f-iso X lt) {x} ⟪ ωx , ⟪ ωx1 , iso ⟫ ⟫ = le00 where
|
|
|
186 le00 : odef X x
|
|
|
187 le00 = subst (λ k → odef X k) &iso ( ω→2f≡i1 _ _ ωx1 lt (iso ωx1) )
|
|
1300
|
188 eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef Omega k) &iso le02 , ⟪ le02 , le01 ⟫ ⟫ where
|
|
|
189 le02 : Omega ∋ * x
|
|
|
190 le02 = power→ Omega _ lt (subst (λ k → odef X k) (sym &iso) Xx)
|
|
|
191 le01 : (wx : odef Omega (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
|
|
1100
|
192 le01 wx with ODC.∋-p O X (nat→ω (ω→nat _ wx) )
|
|
|
193 ... | yes p = refl
|
|
|
194 ... | no ¬p = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where
|
|
|
195 le03 : x ≡ & (nat→ω (ω→nato wx))
|
|
|
196 le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
|
|
|
197
|
|
1099
|
198 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f
|
|
1100
|
199 fω→2-iso f = f-extensionality (λ x → le01 x ) where
|
|
1099
|
200 le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
|
|
1100
|
201 le01 x with ODC.∋-p O (fω→2 f) (nat→ω x)
|
|
|
202 le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where
|
|
1300
|
203 le02 : Omega-d (& (* (& (nat→ω x))))
|
|
1100
|
204 le02 = proj1 (proj2 p )
|
|
|
205 le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where
|
|
|
206 le04 : ¬ f x ≡ i1
|
|
1300
|
207 le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → Omega-d k) (sym &iso) (ω∋nat→ω {x}) , le05 ⟫ ⟫ where
|
|
|
208 le05 : (lt : Omega-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
|
|
1100
|
209 le05 lt = trans (cong f (ω→nat-iso0 x lt (trans *iso *iso))) fx=1
|
|
1099
|
210
|
