annotate filter.agda @ 382:c3a0fb13e267

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Jul 2020 21:32:58 +0900
parents d2cb5278e46d
children 5994f10d9bfd
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
9 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
10 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
11 open import Data.Empty
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
14 open import Relation.Binary.PropositionalEquality
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
16 import BAlgbra
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
18 open BAlgbra O
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
19
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
20 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open OD.OD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
23 open ODAxiom odAxiom
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
25 import ODC
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
26
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
27 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
28 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
29 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
30
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
31 -- Kunen p.76 and p.53, we use ⊆
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
32 record Filter ( L : HOD ) : Set (suc n) where
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
33 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
34 filter : HOD
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
35 f⊆PL : filter ⊆ Power L
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
37 filter2 : { p q : HOD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
38
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
39 open Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
40
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
42 field
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
43 proper : ¬ (filter P ∋ od∅)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
45
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
47 field
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
48 proper : ¬ (filter P ∋ od∅)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
49 ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) )
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
50
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
51 open _⊆_
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
52
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
53 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
55
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
56 refl-⊆ : {A : HOD} → A ⊆ A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
57 refl-⊆ {A} = record { incl = λ x → x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
58
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
59 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
60 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
61 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
62 t1 = zf.IsZF.power→ isZF A t PA∋t
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
63
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
64 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
65 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
66
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
67 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
68 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
69
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
70 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
71 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
72
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
73 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
74 q∩q⊆q = record { incl = λ lt → proj1 lt }
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
75
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
76 open HOD
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
77
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
78 -----
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
79 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
80 -- ultra filter is prime
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
81 --
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
82
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
83 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
84 filter-lemma1 {L} P u = record {
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
85 proper = ultra-filter.proper u
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
86 ; prime = lemma3
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
87 } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
88 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
89 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
90 ... | case1 p∈P = case1 p∈P
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
91 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
92 lemma5 : ((p ∪ q ) ∩ (L \ p)) =h= (q ∩ (L \ p))
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
93 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
94 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
95 } where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
96 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L \ p)) x → odef q x
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
97 lemma4 x lt with proj1 lt
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
98 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
99 lemma4 x lt | case2 qx = qx
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
100 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L \ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
101 lemma6 = filter2 P lt ¬p∈P
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
102 lemma7 : filter P ∋ (q ∩ (L \ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
103 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
104 lemma8 : (q ∩ (L \ p)) ⊆ q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
105 lemma8 = q∩q⊆q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
106
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
107 -----
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
108 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
109 -- if Filter contains L, prime filter is ultra
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
110 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
111
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
112 filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
113 filter-lemma2 {L} P f∋L prime = record {
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
114 proper = prime-filter.proper prime
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
115 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L)
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
116 } where
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
117 open _==_
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
118 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p))
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
119 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
120 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
121 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
122 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x ))
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
123 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
124 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L \ p))
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
125 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
126
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
127 record Dense (P : HOD ) : Set (suc n) where
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
128 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
129 dense : HOD
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
130 d⊆P : dense ⊆ Power P
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
131 dense-f : HOD → HOD
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
132 dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
133 dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p)
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
134
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
135 record Ideal ( L : HOD ) : Set (suc n) where
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
136 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
137 ideal : HOD
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
138 i⊆PL : ideal ⊆ Power L
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
139 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
140 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
141
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
142 open Ideal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
143
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
144 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
145 proper-ideal {L} P {p} = ideal P ∋ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
146
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
147 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
148 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
149
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
150 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
151 field
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
152 filter : L → Set n
371
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 370
diff changeset
153 f⊆P : PL filter
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
154 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q
371
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 370
diff changeset
155 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 370
diff changeset
156
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
157 Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
158 Filter-is-F {L} f = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
159 filter = λ x → Lift (suc n) ((filter f) ∋ x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
160 ; f⊆P = λ x f∋x → power→⊆ _ _ (incl ( f⊆PL f ) (lower f∋x ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
161 ; filter1 = λ {p} {q} q⊆L f∋p p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
162 ; filter2 = λ {p} {q} f∋p f∋q → lift ( filter2 f (lower f∋p) (lower f∋q))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
163 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
164
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
165 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
166 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
167 dense : L → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
168 d⊆P : PL dense
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
169 dense-f : L → L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
170 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
171 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
173 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
174 Dense-is-F {L} f = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
175 dense = λ x → Lift (suc n) ((dense f) ∋ x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
176 ; d⊆P = λ x f∋x → power→⊆ _ _ (incl ( d⊆P f ) (lower f∋x ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
177 ; dense-f = λ x → dense-f f x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
178 ; dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
179 ; dense-p = λ {p} d → dense-p f (d p refl-⊆)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
180 } where open Dense
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
181
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
182 -------
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
183 -- the set of finite partial functions from ω to 2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
184 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
185 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
186
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
187 data Two : Set where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
188 i0 : Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
189 i1 : Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
190
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
191 data Three : Set where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
192 j0 : Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
193 j1 : Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
194 j2 : Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
195
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
196 open import Data.List hiding (map)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
197
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
198 import OPair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
199 open OPair O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
200
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
201 record PFunc {n : Level} : Set (suc n) where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
202 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
203 dom : Nat → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
204 map : (x : Nat ) → dom x → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
206
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
207 open PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
208
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
209 data Findp : List Three → (x : Nat) → Set where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
211 v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
213
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
214 findp : List Three → (x : Nat) → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
215 findp n x = Findp n x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
216
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
217 find : (n : List Three ) → (x : Nat) → Findp n x → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
218 find (j0 ∷ _) 0 v0 = i0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
219 find (j1 ∷ _) 0 v1 = i1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
220 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
221
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
222 Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
223 Findp=n j0 n {x} {p} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
224 Findp=n j1 n {x} {p} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
225 Findp=n j2 n {x} {p} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
227 findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
228 findpeq n {0} {v0} {v0} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
229 findpeq n {0} {v1} {v1} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
230 findpeq [] {Suc x} {()}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
231 findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
232
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
233 3List→PFunc : List Three → PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
234 3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
235
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
236 _3⊆b_ : (f g : List Three) → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
237 [] 3⊆b [] = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
238 [] 3⊆b (j2 ∷ g) = [] 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
239 [] 3⊆b (_ ∷ g) = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
240 (j2 ∷ f) 3⊆b [] = f 3⊆b []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
241 (j2 ∷ f) 3⊆b (_ ∷ g) = f 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
242 (j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
243 (j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
244 _ 3⊆b _ = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
246 _3⊆_ : (f g : List Three) → Set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
247 f 3⊆ g = (f 3⊆b g) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
248
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
249 _3∩_ : (f g : List Three) → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
250 [] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
251 [] 3∩ g = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
252 (j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
253 f 3∩ [] = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
254 (j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
255 (j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
256 (_ ∷ f) 3∩ (_ ∷ g) = j2 ∷ ( f 3∩ g )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
257
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
258 3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
259 3∩⊆f {[]} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
260 3∩⊆f {[]} {j0 ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
261 3∩⊆f {[]} {j1 ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
262 3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
263 3∩⊆f {j0 ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
264 3∩⊆f {j1 ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
265 3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
266 3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
267 3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
268 3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
269 3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
270 3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
271 3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
272 3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
273 3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
274 3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
275
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
276 3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
277 3∩sym {[]} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
278 3∩sym {[]} {j0 ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
279 3∩sym {[]} {j1 ∷ g} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
280 3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
281 3∩sym {j0 ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
282 3∩sym {j1 ∷ f} {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
283 3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
284 3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
285 3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
286 3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
287 3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
288 3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
289 3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
290 3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
291 3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
292 3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
294 3⊆-[] : { h : List Three } → [] 3⊆ h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
295 3⊆-[] {[]} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
296 3⊆-[] {j0 ∷ h} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
297 3⊆-[] {j1 ∷ h} = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
298 3⊆-[] {j2 ∷ h} = 3⊆-[] {h}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
300 3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
301 3⊆trans {[]} {[]} {[]} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
302 3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
303 3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
304 3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
305 3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
306 3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
307 3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
308 3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
309 3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
310 3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
311 3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
312 3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
313 3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
314 3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
315 3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
316 3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
317 3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
318 3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
319 3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g ()
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
320 3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
321 3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
322 3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
323 3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
324 3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
325 3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
326 3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
327 3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
328 3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
329
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
330 3⊆∩f : { f g h : List Three } → f 3⊆ g → f 3⊆ h → f 3⊆ (g 3∩ h )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
331 3⊆∩f {[]} {[]} {[]} f<g f<h = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
332 3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
333 3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
334 3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
335 3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
336 3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
337 3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
338 3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
339 3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
340 3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
341 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
342 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
343 3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
344 3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
345 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
346 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
347 3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
348 3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
349 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
350 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
351 3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
352
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
353 ↑app :(Nat → Two) → Nat → List Three → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
354 ↑app f Zero y = y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
355 ↑app f (Suc x) y with f x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
356 ... | i0 = ↑app f x (j0 ∷ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
357 ... | i1 = ↑app f x (j1 ∷ y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
358
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
359 _3↑_ : (Nat → Two) → Nat → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
360 f 3↑ x = ↑app f x []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
361
382
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
362 3↑22 : (f : Nat → Two) (i j : Nat) → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
363 3↑22 f Zero j = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
364 3↑22 f (Suc i) j with f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
365 3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
366 3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
367
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
368 3↑2 : (Nat → Two) → Nat → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
369 3↑2 f i = 3↑22 f i 0
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
370
382
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
371 lemma10 : (s t : List Three ) → (s 3⊆ t) → ((j0 ∷ s) 3⊆ (j0 ∷ t))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
372 lemma10 s t eq = eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
373 lemma11 : (s t : List Three ) → (s 3⊆ t) → ((j1 ∷ s) 3⊆ (j1 ∷ t))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
374 lemma11 s t eq = eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
375 lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
376 lemma12 s t eq = eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
377 lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
378 lemma13 s t eq = eq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
379 lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
380 lemma14 s t eq = eq
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
381
382
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
382 3↑<2 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑2 f x) 3⊆ (3↑2 f y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
383 3↑<2 {f} {x} {y} x<y = lemma x 0 y x<y (3↑22 f x 0) (3↑22 f y 0) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
384 lemma : (i j y : Nat) → i ≤ y → (s t : List Three) → s 3⊆ t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
385 lemma Zero j y z≤n [] [] = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
386 lemma Zero j y z≤n [] (x ∷ t) = 3⊆-[] {x ∷ t}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
387 lemma Zero j y z≤n (x ∷ s) [] = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
388 lemma Zero j y z≤n (j0 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
389 lemma Zero j y z≤n (j0 ∷ s) (j1 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
390 lemma Zero j y z≤n (j0 ∷ s) (j2 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
391 lemma Zero j y z≤n (j1 ∷ s) (j0 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
392 lemma Zero j y z≤n (j1 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
393 lemma Zero j y z≤n (j1 ∷ s) (j2 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
394 lemma Zero j y z≤n (j2 ∷ s) (j0 ∷ t) = lemma Zero j y z≤n s t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
395 lemma Zero j y z≤n (j2 ∷ s) (j1 ∷ t) = lemma Zero j y z≤n s t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
396 lemma Zero j y z≤n (j2 ∷ s) (j2 ∷ t) = lemma Zero j y z≤n s t
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
397 lemma (Suc i) j (Suc y) (s≤s i<y) [] t = 3⊆-[] {t}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
398 lemma (Suc i) j (Suc y) (s≤s i<y) (x ∷ s) [] = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
399 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j0 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
400 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j1 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
401 lemma (Suc i) j (Suc y) (s≤s i<y) (j0 ∷ s) (j2 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
402 lemma (Suc i) j (Suc y) (s≤s i<y) (j1 ∷ s) (x1 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
403 lemma (Suc i) j (Suc y) (s≤s i<y) (j2 ∷ s) (x1 ∷ t) = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 381
diff changeset
404 -- with lemma i j y i<y s t
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
405
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
406
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
407 3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x) 3⊆ (f 3↑ y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
408 3↑< {f} {x} {y} x<y = {!!} where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
409 lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
410 lemma0 i y with f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
411 lemma0 i y | i0 = case1 refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
412 lemma0 i y | i1 = case2 refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
413 lemma : (i : Nat) → (f 3↑ i) 3⊆ (f 3↑ Suc i)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
414 lemma i with f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
415 lemma i | i0 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
416 lemma i | i1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
418 record Finite3 (p : List Three ) : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
419 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
420 3-max : Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
421 3-func : Nat → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
422 3-p⊆f : p 3⊆ (3-func 3↑ 3-max)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
423 3-f⊆p : (3-func 3↑ 3-max) 3⊆ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
424
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
425 Finite3b : (p : List Three ) → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
426 Finite3b [] = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
427 Finite3b (j0 ∷ f) = Finite3b f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
428 Finite3b (j1 ∷ f) = Finite3b f
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
429 Finite3b (j2 ∷ f) = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
430
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
431 finite3cov : (p : List Three ) → List Three
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
432 finite3cov [] = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
433 finite3cov (j0 ∷ x) = j0 ∷ finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
434 finite3cov (j1 ∷ x) = j1 ∷ finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
435 finite3cov (j2 ∷ x) = j0 ∷ finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
436
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
437 Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
438 Dense-3 = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
439 dense = λ x → Finite3b x ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
440 ; d⊆P = OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
441 ; dense-f = λ x → finite3cov x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
442 ; dense-d = λ {p} d → lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
443 ; dense-p = λ {p} d → lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
444 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
445 lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
446 lemma1 [] = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
447 lemma1 (j0 ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
448 lemma1 (j1 ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
449 lemma1 (j2 ∷ p) = lemma1 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
450 lemma2 : (p : List Three) → p 3⊆ finite3cov p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
451 lemma2 [] = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
452 lemma2 (j0 ∷ p) = lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
453 lemma2 (j1 ∷ p) = lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
454 lemma2 (j2 ∷ p) = lemma2 p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
455
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
456 record 3Gf (f : Nat → Two) (p : List Three ) : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
457 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
458 3gn : Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
459 3f<n : (f 3↑ 3gn) 3⊆ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
460
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
461 open 3Gf
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
462
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
463 min = Data.Nat._⊓_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
464 -- m≤m⊔n = Data.Nat._⊔_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
465 open import Data.Nat.Properties
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
466
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
467 3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
468 3GF {n} f = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
469 filter = λ p → 3Gf f p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
470 ; f⊆P = OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
471 ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
472 ; filter2 = λ {p} {q} fp fq → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
473 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
474 lemma1 : (p q : List Three ) → (fp : 3Gf f p) → (p⊆q : p 3⊆ q) → 3Gf f q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
475 lemma1 p q fp p⊆q = record { 3gn = 3gn fp ; 3f<n = 3⊆trans {f 3↑ 3gn fp } {p} {q} (3f<n fp) p⊆q }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
476 lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q) → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
477 lemma2 p q fp fq = 3⊆∩f {f 3↑ min (3gn fp) (3gn fq) } {p} {q} (3⊆trans {bb} {f 3↑ (3gn fp)} {p} (3↑< {_} {bm} (m⊓n≤m _ _ )) (3f<n fp))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
478 (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq)) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
479 bb = f 3↑ min (3gn fp) (3gn fq)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
480 bm = min (3gn fp) (3gn fq)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
481
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
482 record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
483 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
484 extend : {x : Nat} → (fr : dom f x ) → dom g x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
485 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
486
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
487 open _f⊆_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
488
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
489 _f∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n}
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
490 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
491 ; map = λ x p → map f x (proj1 p) ; meq = meq f }
375
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
492
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
493 _↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
494 _↑_ {n} f i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl }
375
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
495
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
496 record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where
375
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
497 field
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
498 gn : Nat
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
499 f<n : (f ↑ gn) f⊆ p
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
500
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
501 record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
502 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
503 f-max : Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
504 f-func : Nat → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
505 f-p⊆f : p f⊆ (f-func ↑ f-max)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
506 f-f⊆p : (f-func ↑ f-max) f⊆ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
508 open FiniteF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
509
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
510 -- Dense-Gf : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
511 -- Dense-Gf = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
512 -- dense = λ x → FiniteF x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
513 -- ; d⊆P = lift OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
514 -- ; dense-f = λ x → record { dom = {!!} ; map = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
515 -- ; dense-d = λ {p} d → {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
516 -- ; dense-p = λ {p} d → {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
517 -- }
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
518
375
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
519 open Gf
8cade5f660bd Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 374
diff changeset
520
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
521 GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n}) ) _f⊆_ _f∩_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
522 GF {n} f = record {
372
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
523 filter = λ p → Gf f p
374
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
524 ; f⊆P = lift OneObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
525 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 373
diff changeset
526 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
372
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
527 } where
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
528 f1 : {p q : PFunc {n} } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
529 f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
530 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
531 lemma {x} {fr} = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
532 map (f ↑ gn fp) x fr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
533 ≡⟨ feq (f<n fp ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
534 map p x (extend (f<n fp) fr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
535 ≡⟨ feq p⊆q ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
536 map q x (extend p⊆q (extend (f<n fp) fr))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
537 ∎ where open ≡-Reasoning
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
538 f2 : {p q : PFunc {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q)
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
539 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
540 fmin : PFunc {n}
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
541 fmin = f ↑ (min (gn fp) (gn fq))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
542 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
543 lemma1 {x} x<g fr gr = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
544 map p x fr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
545 ≡⟨ meq p ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
546 map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
547 ≡⟨ sym (feq (f<n fp)) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
548 map (f ↑ (min (gn fp) (gn fq))) x x<g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
549 ≡⟨ feq (f<n fq) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
550 map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
551 ≡⟨ meq q ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
552 map q x gr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
553 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
554 lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
555 lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
556 proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
557 f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
558 f∩→⊆ p q = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
559 extend = λ {x} pq → proj1 (proj2 pq)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
560 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
561 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
562 lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
563 lemma3 {x} fr =
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
564 map (f ↑ min (gn fp) (gn fq)) x fr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
565 ≡⟨ feq (f<n fq) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
566 map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
567 ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
568 map (p f∩ q) x (lemma2 fr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
569 ∎ where open ≡-Reasoning
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
570
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
571
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
572 ODSuc : (y : HOD) → infinite ∋ y → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
573 ODSuc y lt = Union (y , (y , y))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
574
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
575 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
576 hφ : Hω2 0 o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
577 h0 : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
578 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
579 h1 : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
580 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
581 he : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
582 Hω2 (Suc i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
583
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
584 record Hω2r (x : Ordinal) : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
585 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
586 count : Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
587 hω2 : Hω2 count x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
588
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
589 open Hω2r
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
590
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
591 HODω2 : HOD
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
592 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
593 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
594 ω<next = ω<next-o∅ ho<
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
595 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
596 lemma = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
597 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
598 odmax0 {y} r with hω2 r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
599 ... | hφ = x<nx
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
600 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
601 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
602 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
603
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
604 ω→2 : HOD
379
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 375
diff changeset
605 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
606 repl : HOD → HOD → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
607 repl p x with ODC.∋-p O p x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
608 ... | yes _ = nat→ω 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
609 ... | no _ = nat→ω 0
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
610
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
611 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
612 -- field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
613 -- n : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
614 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
615
372
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
616 -- Gf : {f : HOD} → ω→2 ∋ f → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 371
diff changeset
617 -- Gf {f} lt = Select HODω2 (λ x H∋x → {!!} )
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
618
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
619 G : (Nat → Two) → Filter HODω2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
620 G f = record {
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
621 filter = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
622 ; f⊆PL = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
623 ; filter1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
624 ; filter2 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
625 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
626 filter0 : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
627 filter0 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
628 f⊆PL1 : filter0 ⊆ Power HODω2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
629 f⊆PL1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
630 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
631 filter11 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
632 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
633 filter12 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
634
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
635 -- the set of finite partial functions from ω to 2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
636
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
637 Hω2f : Set (suc n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
638 Hω2f = (Nat → Set n) → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
639
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
640 Hω2f→Hω2 : Hω2f → HOD
381
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 380
diff changeset
641 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
642
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
643