Mercurial > hg > Members > kono > Proof > category

comparison src/Polynominal.agda @ 1079:d07cfce03236

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 May 2021 00:42:14 +0900
parents 5aa36440e6fe
children c61639f34e7b
comparison
equal deleted inserted replaced
1078:5aa36440e6fe 1079:d07cfce03236
73 -- case i i is π ∙ f ≈ π ∙ g 73 -- case i i is π ∙ f ≈ π ∙ g
74 -- we have (x y : Hom A １ a) → x ≡ y (minimul equivalende assumption). this makes all k x ii case valid 74 -- we have (x y : Hom A １ a) → x ≡ y (minimul equivalende assumption). this makes all k x ii case valid
75 -- all other cases, arguments are reduced to f ∙ π' . 75 -- all other cases, arguments are reduced to f ∙ π' .
76 --postulate 76 --postulate
77 -- x-singleon : {a b c : Obj A} → (f : Poly a c b ) → (x y : Hom A b a) → x ≡ y -- minimul equivalende assumption (variables are the same except its name) 77 -- x-singleon : {a b c : Obj A} → (f : Poly a c b ) → (x y : Hom A b a) → x ≡ y -- minimul equivalende assumption (variables are the same except its name)
78 k-cong : {a b c : Obj A} → (f g : Poly a c b )
79 → Poly.x f ≡ Poly.x g
80 → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ]
81 k-cong {a} {b} {c} f g refl f=f with Poly.x f | (Poly.phi f) | (Poly.phi g)
82 ... | x | i {_} {_} {f'} | i = resp refl-hom f=f
83 ... | x | i {_} {_} {f'} | ii = {!!}
84 ... | x | i {_} {_} {h} | iii {_} {_} {_} {f₁} {g₁} t t₁ = begin
85 k x {h} i ≈⟨⟩
86 h ∙ π' ≈⟨ car f=f ⟩
87 < f₁ , g₁ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
88 < f₁ ∙ π' , g₁ ∙ π' > ≈⟨⟩
89 < k x {f₁} i , k x {g₁} i > ≈⟨ IsCCC.π-cong isCCC (k-cong _ _ refl {!!} ) {!!} ⟩
90 < k x t , k x t₁ > ≈⟨⟩
91 k x (iii t t₁) ∎
92 ... | x | i {_} {_} {f'} | iv t t₁ = {!!}
93 ... | x | i {_} {_} {f'} | v t = {!!}
94 ... | x | i {_} {_} {f'} | φ-cong x₁ t = {!!}
95 ... | _ | ii | t = {!!}
96 ... | x | iii s s₁ | t = {!!}
97 ... | x | iv s s₁ | t = {!!}
98 ... | x | v s | t = {!!}
99 ... | x | φ-cong x₁ s | t = {!!}
100
101 -- we may prove k-cong from x-singleon 78 -- we may prove k-cong from x-singleon
102 -- k-cong' : {a b c : Obj A} → (f g : Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ] 79 -- k-cong' : {a b c : Obj A} → (f g : Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ]
103 -- k-cong' {a} {b} {c} f g f=g with Poly.phi f | Poly.phi g 80 -- k-cong' {a} {b} {c} f g f=g with Poly.phi f | Poly.phi g
104 81
105 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future 82 -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
136 -- we should open IsCCC isCCC 113 -- we should open IsCCC isCCC
137 π-cong = IsCCC.π-cong isCCC 114 π-cong = IsCCC.π-cong isCCC
138 *-cong = IsCCC.*-cong isCCC 115 *-cong = IsCCC.*-cong isCCC
139 distr-* = IsCCC.distr-* isCCC 116 distr-* = IsCCC.distr-* isCCC
140 e2 = IsCCC.e2 isCCC 117 e2 = IsCCC.e2 isCCC
118 idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a ≈ id1 A a
119 idx {a} {x} = begin
120 x ∙ ○ a ≈⟨ {!!} ⟩
121 id1 A a ∎
141 122
142 -- proof in p.59 Lambek 123 -- proof in p.59 Lambek
143 functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p 124 functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p
144 functional-completeness {a} {b} {c} p = record { 125 functional-completeness {a} {b} {c} p = record {
145 fun = k (Poly.x p) (Poly.phi p) 126 fun = k (Poly.x p) (Poly.phi p)
199 f * ∎ 180 f * ∎
200 ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 x f y ) f=f' 181 ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 x f y ) f=f'
201 -- 182 --
202 -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p) 183 -- f ∙ < x ∙ ○ b , id1 A b > ≈ f → f ≈ k x (phi p)
203 -- 184 --
185 ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → A [ f ∙ π' ≈ k x fp ]
186 ki x f i = refl-hom
187 ki {a} x .x ii = begin
188 x ∙ π' ≈⟨ {!!} ⟩
189 x ∙ ○ (a ∧ １) ≈⟨ {!!} ⟩
190 x ∙ (○ a ∙ π ) ≈⟨ {!!} ⟩
191 (x ∙ ○ a ) ∙ π ≈⟨ {!!} ⟩
192 id1 A a ∙ π ≈⟨ {!!} ⟩
193 k x ii ∎
194 ki x .(< f₁ , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
195 < f₁ , f₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
196 < f₁ ∙ π' , f₂ ∙ π' > ≈⟨ π-cong (ki x f₁ fp₁) (ki x f₂ fp₂) ⟩
197 k x (iii fp₁ fp₂ ) ∎
198 ki x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
199 (f₁ ∙ f₂ ) ∙ π' ≈⟨ {!!} ⟩
200 f₁ ∙ ( f₂ ∙ π') ≈⟨ {!!} ⟩
201 f₁ ∙ ( π' ∙ < π , (f₂ ∙ π' ) >) ≈⟨ {!!} ⟩
202 (f₁ ∙ π' ) ∙ < π , (f₂ ∙ π' ) > ≈⟨ {!!} ⟩
203 k x fp ∙ < π , k x fp₁ > ≈⟨⟩
204 k x (iv fp fp₁ ) ∎
205 ki x .((C CCC.*) _) (v fp) = {!!}
206 ki x f (φ-cong x₁ fp) = {!!}
204 uniq : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) → 207 uniq : {a b c : Obj A} → (x : Hom A １ a) (f : Hom A b c) (phi : φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) →
205 A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ] 208 A [ f' ∙ < x ∙ ○ b , id1 A b > ≈ f ] → A [ f' ≈ k x phi ]
206 uniq {a} {b} {c} x f phi f' fx=p = sym (begin 209 uniq {a} {b} {c} x f phi f' fx=p = sym (begin
207 k x phi ≈↑⟨ k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = phi } refl fx=p ⟩ 210 k x phi ≈↑⟨ ki x f phi ⟩
211 k x {f} i ≈↑⟨ car fx=p ⟩
208 k x {f' ∙ < x ∙ ○ b , id1 A b >} i ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π' 212 k x {f' ∙ < x ∙ ○ b , id1 A b >} i ≈⟨ trans-hom (sym assoc) (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π'
209 f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii i i ) -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) 213 f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii i i ) -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > )
210 ≈⟨ cdr (π-cong (k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = iv ii i } refl refl-hom ) refl-hom) ⟩ 214 ≈⟨ cdr (π-cong (ki x ( x ∙ ○ b) (iv ii i) ) refl-hom) ⟩
211 f' ∙ < k x {x ∙ ○ b} (iv ii i ) , k x {id1 A b} i > ≈⟨ refl-hom ⟩ 215 f' ∙ < k x {x ∙ ○ b} (iv ii i ) , k x {id1 A b} i > ≈⟨ refl-hom ⟩
212 f' ∙ < k x {x} ii ∙ < π , k x {○ b} i > , k x {id1 A b} i > -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' > , id1 A b ∙ π' > ) 216 f' ∙ < k x {x} ii ∙ < π , k x {○ b} i > , k x {id1 A b} i > -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' > , id1 A b ∙ π' > )
213 ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ 217 ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩
214 f' ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩ 218 f' ∙ < π ∙ < π , (○ b ∙ π' ) > , π' > ≈⟨ cdr (π-cong (IsCCC.e3a isCCC) refl-hom) ⟩
215 f' ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩ 219 f' ∙ < π , π' > ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
216 f' ∙ id1 A _ ≈⟨ idR ⟩ 220 f' ∙ id1 A _ ≈⟨ idR ⟩
217 f' ∎ ) 221 f' ∎ )
222
223 ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp : φ x {b} {c} f ) → A [ f ∙ π' ≈ k x fp ]
224 ki = {!!}
225 k-cong : {a b c : Obj A} → (f g : Poly a c b )
226 → Poly.x f ≡ Poly.x g
227 → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f) ≈ k (Poly.x g) (Poly.phi g) ]
228 k-cong {a} {b} {c} f g refl f=f = kcong (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where
229 kcong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp : φ x {b} {c} f )( gp : φ x {b} {c} g ) → A [ k x fp ≈ k x gp ]
230 kcong {a} {b} {c} x f g f=g i i = resp refl-hom f=g
231 kcong {a} {.(CCC.１ C)} {.a} x f .x f=g i ii = begin
232 k x {f} i ≈⟨⟩
233 f ∙ π' ≈⟨ car f=g ⟩
234 x ∙ π' ≈⟨ ki x x ii ⟩
235 k x ii ∎
236 kcong {a} {b} {.((C CCC.∧ _) _)} x f .(< g₁ , g₂ >) f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin
237 k x i ≈⟨ car f=g ⟩
238 < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
239 < g₁ ∙ π' , g₂ ∙ π' > ≈⟨ IsCCC.π-cong isCCC (ki x _ gp₁ ) (ki x _ gp₂) ⟩
240 < k x gp₁ , k x gp₂ > ≈⟨⟩
241 k x (iii gp₁ gp₂) ∎
242 kcong {a} {b} {c} x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!}
243 kcong {a} {b} {.((C CCC.<= _) _)} x f .((C CCC.*) _) f=g i (v gp) = {!!}
244 kcong {a} {b} {c} x f g f=g i (φ-cong x₁ gp) = {!!}
245 kcong {a} {.(CCC.１ C)} {.a} x .x g f=g ii gp = {!!}
246 kcong {a} {b} {.((C CCC.∧ _) _)} x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!}
247 kcong {a} {b} {c} x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!}
248 kcong {a} {b} {.((C CCC.<= _) _)} x .((C CCC.*) _) g f=g (v fp) gp = {!!}
249 kcong {a} {b} {c} x f g f=g (φ-cong x₁ fp) gp = {!!}
250
218 251
219 -- functional completeness ε form 252 -- functional completeness ε form
220 -- 253 --
221 -- g : Hom A １ (b <= a) fun : Hom A (a ∧ １) c 254 -- g : Hom A １ (b <= a) fun : Hom A (a ∧ １) c
222 -- fun * ε ∙ < g ∙ π , π' > 255 -- fun * ε ∙ < g ∙ π , π' >