|
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 zf
|
|
|
7 open import logic
|
|
|
8 -- open import partfunc {n} O
|
|
|
9 import OD
|
|
|
10
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary
|
|
|
13 open import Data.Empty
|
|
|
14 open import Relation.Binary
|
|
|
15 open import Relation.Binary.Core
|
|
|
16 open import Relation.Binary.PropositionalEquality
|
|
|
17 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
18 import BAlgbra
|
|
|
19
|
|
|
20 open BAlgbra O
|
|
|
21
|
|
|
22 open inOrdinal O
|
|
|
23 open OD O
|
|
|
24 open OD.OD
|
|
|
25 open ODAxiom odAxiom
|
|
|
26 import OrdUtil
|
|
|
27 import ODUtil
|
|
|
28 open Ordinals.Ordinals O
|
|
|
29 open Ordinals.IsOrdinals isOrdinal
|
|
|
30 open Ordinals.IsNext isNext
|
|
|
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
|
|
|
54 import OPair
|
|
|
55 open OPair O
|
|
|
56
|
|
|
57 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
|
|
|
58 hφ : Hω2 0 o∅
|
|
|
59 h0 : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
|
60 Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) , * x )))
|
|
|
61 h1 : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
|
62 Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) , * x )))
|
|
|
63 he : {i : Nat} {x : Ordinal } → Hω2 i x →
|
|
|
64 Hω2 (Suc i) x
|
|
|
65
|
|
|
66 record Hω2r (x : Ordinal) : Set n where
|
|
|
67 field
|
|
|
68 count : Nat
|
|
|
69 hω2 : Hω2 count x
|
|
|
70
|
|
|
71 open Hω2r
|
|
|
72
|
|
|
73 HODω2 : HOD
|
|
|
74 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
|
|
|
75 P : (i j : Nat) (x : Ordinal ) → HOD
|
|
|
76 P i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x
|
|
|
77 nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
|
|
|
78 nat1 i x = next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
|
|
|
79 lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x
|
|
|
80 lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
|
|
|
81 (subst (λ k → k o< next x) (sym &iso) x<nx ))
|
|
|
82 lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x
|
|
|
83 lemma i j x = next< (lemma1 i j x ) ho<
|
|
|
84 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅
|
|
|
85 odmax0 {y} r with hω2 r
|
|
|
86 ... | hφ = x<nx
|
|
|
87 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
|
|
|
88 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
|
|
|
89 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
|
|
|
90
|
|
|
91 3→Hω2 : List (Maybe Two) → HOD
|
|
|
92 3→Hω2 t = list→hod t 0 where
|
|
|
93 list→hod : List (Maybe Two) → Nat → HOD
|
|
|
94 list→hod [] _ = od∅
|
|
|
95 list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) ))
|
|
|
96 list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) ))
|
|
|
97 list→hod (nothing ∷ t) i = list→hod t (Suc i )
|
|
|
98
|
|
|
99 Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two)
|
|
|
100 Hω2→3 x = lemma where
|
|
|
101 lemma : { y : Ordinal } → Hω2r y → List (Maybe Two)
|
|
|
102 lemma record { count = 0 ; hω2 = hφ } = []
|
|
|
103 lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 }
|
|
|
104 lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 = hω3 }
|
|
|
105 lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 }
|
|
|
106
|
|
|
107 ω→2 : HOD
|
|
|
108 ω→2 = Power infinite
|
|
|
109
|
|
|
110 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
|
|
|
111 ω→2f x lt n with ODC.∋-p O x (nat→ω n)
|
|
|
112 ω→2f x lt n | yes p = i1
|
|
|
113 ω→2f x lt n | no ¬p = i0
|
|
|
114
|
|
|
115 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
|
|
|
116 fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (& x) ) → f (ω→nat x lt) ≡ i1 )
|
|
|
117
|
|
|
118 fω→2 : (Nat → Two) → HOD
|
|
|
119 fω→2 f = Select infinite (fω→2-sel f)
|
|
|
120
|
|
|
121 open _==_
|
|
|
122
|
|
|
123 import Axiom.Extensionality.Propositional
|
|
|
124 postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m
|
|
|
125
|
|
|
126 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
|
|
|
127 ω2∋f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
|
|
|
128
|
|
|
129 ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i
|
|
|
130 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
|
|
|
131 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
|
|
|
132
|
|
|
133 -- someday ...
|
|
|
134 -- postulate
|
|
|
135 -- ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X
|
|
|
136 -- fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
|
|
|
137
|
