## corque / lemma_9.v @ 4806fe22

History | View | Annotate | Download (53.8 KB)

1 |
Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/". |
---|---|

2 |
Require Import biCCC. |

3 |
Require Import Lemmas_biCCC. |

4 |
Require Import ElgotMonad. |

5 |
Require Import Lemmas_ElgotMonad. |

6 |
Require Import CofreeElgotMonad. |

7 |
Require Import Lemmas_CofreeElgotMonad. |

8 |
Require Import Coq_Steroids. |

9 |
Require Import Setoid. |

10 |
Open Scope c_scope. |

11 | |

12 |
Section ContextCofreeElgotMonad. |

13 |
Context `(Co: CofreeElgotMonad). |

14 | |

15 |
Parameter a b : Obj. |

16 | |

17 |
(* --- *) |

18 | |

19 | |

20 |
Theorem proving_kl1 : forall |

21 |
(x : Obj), |

22 |
(ηv (x:=x) (a:=a) (b:=b)) § = id. |

23 | |

24 |
Proof. |

25 |
intros. |

26 |
symmetry; apply lifting2; rewrite -> id_l. |

27 |
rewrite -> out_unitcofree. |

28 |
rewrite -> cont_id, -> id_l. |

29 |
rewrite <- f_cpr, -> inl_inr_is_id, id_l. |

30 |
rewrite -> kl1, id_r; trivial. |

31 |
Qed. |

32 | |

33 | |

34 | |

35 |
Theorem proving_kl2 : forall |

36 |
(x y : Obj) |

37 |
(f: x ~> coext T a b y), |

38 |
f § ∘ ηv (x:=x) = f. |

39 | |

40 |
Proof. |

41 |
intros. |

42 |
apply out_cong. |

43 |
rewrite -> comp_assoc, lifting1. |

44 |
rewrite <- comp_assoc, -> out_unitcofree. |

45 |
rewrite -> comp_assoc, kl2. |

46 |
rewrite -> cpr_inl; trivial. |

47 |
Qed. |

48 | |

49 | |

50 | |

51 |
Theorem proving_kl3 : forall |

52 |
(x y z : Obj) |

53 |
(f : y ~> coext T a b z) |

54 |
(g : x ~> coext T a b y), |

55 |
(f § ∘ g) § = f § ∘ g §. |

56 | |

57 |
Proof. |

58 |
intros. |

59 |
symmetry; apply lifting2. |

60 |
rewrite -> comp_assoc, lifting1. |

61 |
rewrite <- comp_assoc, -> lifting1. |

62 | |

63 |
rewrite -> comp_assoc with (f':=out); apply f_equal2; trivial. |

64 |
rewrite <- kl3; apply f_equal1. |

65 | |

66 |
rewrite -> f_cpr. |

67 |
rewrite <- comp_assoc with (f':=cont (g §)), -> comp_assoc with (g':=η), -> kl2. |

68 |
rewrite -> comp_assoc with (g':=inr), cpr_inr. |

69 |
rewrite <- comp_assoc with (f':=cont (g §)), -> cont_comp. |

70 | |

71 |
rewrite -> comp_assoc with (h':=out), -> lifting1. |

72 |
rewrite -> comp_assoc with (f':=g); trivial. |

73 |
Qed. |

74 | |

75 | |

76 | |

77 |
(* additional lemmas based on proving_kl1-3 *) |

78 |
(* at the wrong place, change name? *) |

79 |
Lemma mapc_unfold : forall |

80 |
(x y : Obj) |

81 |
(f:x ~> y), |

82 |
mapc f = (ηv (a:=a) (b:=b) ∘ f) §. |

83 | |

84 |
Proof. |

85 |
intros. |

86 |
unfold mapc. |

87 |
symmetry; apply coit2. |

88 |
rewrite -> comp_assoc, map_comp. |

89 |
rewrite -> coprodhom_comp, id_r, id_l. |

90 |
rewrite -> lifting1. |

91 |
rewrite -> comp_assoc with (h':=out), out_unitcofree. |

92 | |

93 |
unfold map, coprodhom. |

94 |
rewrite -> f_cpr, ->2 comp_assoc; trivial. |

95 |
Qed. |

96 | |

97 | |

98 | |

99 |
Lemma liftingcofree_mapc : forall |

100 |
(x y z : Obj) |

101 |
(f: y ~> coext T a b z) |

102 |
(g: x ~> y), |

103 |
f § ∘ mapc g = (f ∘ g) §. |

104 | |

105 |
Proof. |

106 |
intros. |

107 |
rewrite -> mapc_unfold. |

108 |
rewrite <- proving_kl3. |

109 |
rewrite -> comp_assoc, proving_kl2. |

110 |
trivial. |

111 |
Qed. |

112 | |

113 | |

114 | |

115 |
Lemma mapc_liftingcofree : forall |

116 |
(x y z : Obj) |

117 |
(f: y ~> z) |

118 |
(g: x ~> coext T a b y), |

119 |
mapc f ∘ g § = (mapc f ∘ g) §. |

120 | |

121 |
Proof. |

122 |
intros. |

123 |
rewrite -> mapc_unfold. |

124 |
rewrite <- proving_kl3. |

125 |
trivial. |

126 |
Qed. |

127 | |

128 | |

129 |
(* --- *) |

130 | |

131 | |

132 | |

133 |
Theorem proving_unfolding : forall |

134 |
(x y : Obj) |

135 |
(f : x ~> (coext T a b (y ⊕ x))), |

136 |
[ηv , f †'] § ∘ f = f †'. |

137 | |

138 |
Proof. |

139 |
intros. |

140 |
symmetry; rewrite -> unfolding_triangle1 at 1. |

141 | |

142 |
unfold triangle. |

143 | |

144 |
rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=tuo), -> liftingcofree_tuo. |

145 | |

146 |
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), <- comp_assoc with (h':=tuo), -> lifting_map. |

147 |
rewrite -> cpr_coprodhom, cpr_inl, id_l. |

148 | |

149 |
rewrite <- unfolding. |

150 | |

151 |
rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=(([η, ((π ∘ out) ∘ f) †]) *)). |

152 |
rewrite <- kl3, -> f_cpr, -> kl2. |

153 |
rewrite <- out_itercofree. |

154 | |

155 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=π). |

156 |
unfold π. |

157 |
rewrite -> lifting_map. |

158 |
rewrite -> f_cpr. |

159 |
rewrite -> cpr_coprodhom, cpr_inl, id_l. |

160 |
rewrite -> comp_assoc with (g':=inl), cpr_inl, cpr_inr. |

161 | |

162 |
rewrite ->2 comp_assoc, <- liftingcofree_tuo. |

163 |
rewrite <- comp_assoc with (g':=tuo), -> tuo_out_is_id, id_l; trivial. |

164 | |

165 |
Qed. |

166 | |

167 | |

168 | |

169 |
(* --- *) |

170 | |

171 | |

172 | |

173 |
(* TODO: adjust name? *) |

174 |
Lemma proving_naturality_h1 : forall (x y z : Obj) |

175 |
(h: x ~> coext T a b (y ⊕ x)) |

176 |
(g: y ~> coext T a b z), |

177 |
guarded h -> |

178 |
guarded ([mapc inl ∘ g, ηv ∘ inr] § ∘ h). |

179 | |

180 |
Proof. |

181 |
intros. |

182 |
unfold guarded in H; inversion H as [u' H1]. |

183 | |

184 |
unfold guarded. |

185 | |

186 |
exists ([map (id ⊕⊕ id ×× mapc inl ^^ id) ∘ out ∘ g, η ∘ inr ∘ |

187 |
cont (([mapc inl ∘ g, ηv ∘ inr]) §)] * ∘ u'). |

188 | |

189 |
rewrite -> comp_assoc, lifting1. |

190 | |

191 |
rewrite <- comp_assoc, -> H1. |

192 | |

193 |
rewrite -> comp_assoc with (f':=u'), lifting_map. |

194 |
rewrite -> cpr_coprodhom. |

195 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl, id_l. |

196 |
rewrite -> comp_assoc, out_mapc. |

197 | |

198 |
rewrite -> comp_assoc with (f':=u'); apply f_equal2; trivial. |

199 |
rewrite -> map_lifting; apply f_equal1. |

200 | |

201 |
rewrite -> f_cpr. |

202 |
rewrite ->2 comp_assoc, map_comp, coprodhom_comp, id_l, id_r. |

203 |
rewrite <-2 comp_assoc with (h':=η), -> comp_assoc with (g':=η), map_unit. |

204 |
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (h':=inl ⊕⊕ id). |

205 |
rewrite -> coprodhom_inr, id_l; trivial. |

206 | |

207 |
Qed. |

208 | |

209 | |

210 | |

211 |
(* TODO: change name, move ? *) |

212 |
Theorem proving_naturality_h2 : forall (x y z : Obj) |

213 |
(f : x ~> (coext T a b (y ⊕ x))) |

214 |
(g : y ~> (coext T a b z)), |

215 |
▷(([mapc inl ∘ g, ηv ∘ inr]) § ∘ f) = (([mapc inl ∘ g, ηv ∘ inr]) § ∘ ▷f). |

216 | |

217 |
Proof. |

218 |
intros. |

219 | |

220 |
set (w:=[mapc inl ∘ g, ηv ∘ inr]). |

221 | |

222 |
rewrite <- guardedtriangle; trivial. |

223 | |

224 |
unfold triangle at 2 3. |

225 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1. |

226 |
rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. |

227 |
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map, -> cpr_coprodhom, -> id_l. |

228 |
rewrite <- comp_assoc with (g':=w); unfold w at 2. |

229 |
rewrite -> cpr_inl. |

230 | |

231 |
rewrite -> comp_assoc with (h':=π); unfold π at 1. |

232 |
rewrite -> map_lifting. |

233 |
rewrite -> naturality. |

234 |
rewrite <- codiagonal. |

235 |
rewrite -> comp_assoc with (h':=map ([id, inr])), -> map_lifting. |

236 |
rewrite -> f_cpr. |

237 |
rewrite ->4 comp_assoc, ->2 map_comp. |

238 |
rewrite -> cpr_inl, -> id_r. |

239 |
rewrite -> comp_assoc with (g':=η), -> map_unit. |

240 |
rewrite <- comp_assoc with (f':=inr), -> cpr_inr. |

241 | |

242 |
unfold π. |

243 |
rewrite -> lifting_map. |

244 |
rewrite -> f_cpr. |

245 |
rewrite -> cpr_coprodhom. |

246 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl, -> id_l. |

247 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

248 |
rewrite <- comp_assoc with (f':=inr), -> cpr_inr. |

249 | |

250 |
assert (aux: map ([inl ⊕⊕ id, inl ∘ inr]) ∘ η ∘ inl ∘ inr = |

251 |
η ∘ inr (a:=z ⊕ a × coext T a b (z ⊕ x) ^ b) (b:=x)). |

252 |
rewrite -> map_unit. |

253 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl. |

254 |
rewrite <- comp_assoc, -> coprodhom_inr, -> id_l. |

255 |
trivial. |

256 |
rewrite <- aux; clear aux. |

257 | |

258 |
rewrite <-2 comp_assoc with (h':=map ([inl ⊕⊕ id, inl ∘ inr])), <-2 f_cpr. |

259 |
rewrite <- map_lifting. |

260 |
rewrite <- out_unitcofree. |

261 |
rewrite <- comp_assoc with (h':=out), <- f_cpr. |

262 |
rewrite <- comp_assoc with (f':=out), <- lifting1. |

263 |
rewrite -> comp_assoc with (g':=out), <- comp_assoc with (f':=f). |

264 |
trivial. |

265 | |

266 | |

267 |
apply proving_naturality_h1. |

268 |
apply guardedtriangle_def. |

269 | |

270 |
Qed. |

271 | |

272 | |

273 | |

274 |
Theorem proving_naturality : forall |

275 |
(x y z : Obj) |

276 |
(f : x ~> (coext T a b (y ⊕ x))) |

277 |
(g : y ~> (coext T a b z)), |

278 |
g § ∘ f †' = ([(ηv ∘ inl) § ∘ g , ηv ∘ inr] § ∘ f) †'. |

279 | |

280 |
Proof. |

281 |
intros. |

282 |
rewrite <- mapc_unfold. |

283 | |

284 |
rewrite -> itercofree_triangle. |

285 |
symmetry; rewrite -> itercofree_triangle; symmetry. |

286 | |

287 |
rewrite -> proving_naturality_h2. |

288 | |

289 |
apply unfolding_guarded2. |

290 | |

291 |
apply proving_naturality_h1. |

292 | |

293 |
apply guardedtriangle_def. |

294 | |

295 |
rewrite -> comp_assoc, <- proving_kl3. |

296 |
rewrite -> f_cpr. |

297 |
rewrite -> comp_assoc, -> liftingcofree_mapc. |

298 |
rewrite -> cpr_inl. |

299 |
rewrite -> proving_kl1, -> id_r. |

300 |
rewrite -> comp_assoc, -> proving_kl2. |

301 |
rewrite -> cpr_inr. |

302 | |

303 |
rewrite <- proving_unfolding at 1. |

304 |
rewrite -> comp_assoc, <- proving_kl3. |

305 |
rewrite -> f_cpr. |

306 |
rewrite -> proving_kl2. |

307 |
trivial. |

308 |
Qed. |

309 | |

310 | |

311 | |

312 |
(* --- *) |

313 | |

314 | |

315 | |

316 |
Theorem proving_dinaturality : forall |

317 |
(x y z : Obj) |

318 |
(g: x ~> (coext T a b (y ⊕ z))) |

319 |
(h : z ~> (coext T a b (y ⊕ x))), |

320 |
([ηv ∘ inl , h] § ∘ g) †' = |

321 |
[ ηv , ([ηv ∘ inl , g] § ∘ h) †' ] § ∘ g. |

322 | |

323 |
Proof. |

324 |
intros. |

325 | |

326 |
set (s:=[ηv ∘ inl, h] § ∘ g). |

327 |
set (t:=[ηv ∘ inl, g] § ∘ h). |

328 |
set (w:=[ηv, t †'] § ∘ g). |

329 | |

330 | |

331 |
set (p:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, h] §)) ⊕⊕ id (a:=z)))). |

332 |
set (q:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, g] §)) ⊕⊕ id (a:=x)))). |

333 | |

334 | |

335 |
assert (Hp: (π ∘ out ∘ s) † = |

336 |
([η ∘ inl, π ∘ out ∘ h] * ∘ p ∘ π ∘ out ∘ g) †). |

337 |
apply f_equal1. |

338 |
unfold s. |

339 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

340 |
rewrite <- comp_assoc, -> lifting1. |

341 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

342 |
unfold π at 1. |

343 |
rewrite -> map_lifting. |

344 |
rewrite ->2 f_cpr. |

345 |
rewrite -> comp_assoc with (h':=out), out_unitcofree. |

346 |
rewrite -> f_cpr. |

347 |
rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit. |

348 |
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl. |

349 |
rewrite -> coprodhom_inl. |

350 |
rewrite <- comp_assoc with (g':=inr),-> comp_assoc with (g':=η), map_unit. |

351 |
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), cpr_inr. |

352 |
unfold p, π. |

353 |
rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp. |

354 |
rewrite -> f_cpr. |

355 |
rewrite -> coprodhom_comp, id_l. |

356 |
rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l. |

357 |
rewrite -> comp_assoc with (g':=inl). |

358 |
rewrite -> coprodhom_inl. |

359 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

360 |
rewrite -> lifting_map; apply f_equal1. |

361 |
rewrite -> f_cpr. |

362 |
rewrite -> cpr_coprodhom, id_l. |

363 |
rewrite -> comp_assoc with (g':=inl), cpr_inl. |

364 |
rewrite ->4 comp_assoc; trivial. |

365 | |

366 | |

367 |
assert (Hq: (π ∘ out ∘ t) † = |

368 |
([η ∘ inl, π ∘ out ∘ g] * ∘ q ∘ π ∘ out ∘ h) †). |

369 |
apply f_equal1. |

370 |
unfold t. |

371 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

372 |
rewrite <- comp_assoc, -> lifting1. |

373 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

374 |
unfold π at 1. |

375 |
rewrite -> map_lifting. |

376 |
rewrite ->2 f_cpr. |

377 |
rewrite -> comp_assoc with (h':=out), -> out_unitcofree. |

378 |
rewrite -> f_cpr. |

379 |
rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit. |

380 |
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl. |

381 |
rewrite -> coprodhom_inl. |

382 |
rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit. |

383 |
rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), -> cpr_inr. |

384 |
unfold q, π. |

385 |
rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp. |

386 |
rewrite -> f_cpr. |

387 |
rewrite -> coprodhom_comp, -> id_l. |

388 |
rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l. |

389 |
rewrite -> comp_assoc with (g':=inl), coprodhom_inl. |

390 |
rewrite <- comp_assoc with (f':=inr), coprodhom_inr. |

391 |
rewrite -> lifting_map; apply f_equal1. |

392 |
rewrite -> f_cpr. |

393 |
rewrite -> cpr_coprodhom, id_l. |

394 |
rewrite -> comp_assoc with (g':=inl), cpr_inl. |

395 |
rewrite ->4 comp_assoc; trivial. |

396 | |

397 | |

398 |
assert (H_main: [ηv, w] § ∘ ▷ s = [ηv, t †'] § ∘ [ ηv ∘ inl , ▷ t] § ∘ g). |

399 | |

400 |
(* left-hand side *) |

401 |
apply out_cong. |

402 |
rewrite -> comp_assoc, -> lifting1 at 1. |

403 |
unfold triangle at 1. |

404 |
rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), comp_assoc with (g':=tuo); |

405 |
rewrite -> out_tuo_is_id, id_r. |

406 |
rewrite -> comp_assoc, lifting_map. |

407 |
rewrite -> cpr_coprodhom. |

408 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl. |

409 |
rewrite -> out_unitcofree, id_l. |

410 | |

411 |
rewrite -> Hp. |

412 | |

413 |
rewrite <- comp_assoc with (g':=p), <- comp_assoc with (f':=g), <- comp_assoc with (f':=out ∘ g). |

414 |
rewrite -> dinaturality. |

415 | |

416 |
unfold p at 2. |

417 |
rewrite <- comp_assoc with (h':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id))); |

418 |
rewrite -> comp_assoc with (g':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id))); |

419 |
rewrite -> lifting_map. |

420 |
rewrite -> cpr_coprodhom, id_l. |

421 | |

422 |
rewrite -> comp_assoc, <- kl3. |

423 |
rewrite -> f_cpr. |

424 |
rewrite -> comp_assoc with (g':=η), kl2. |

425 |
rewrite -> cpr_coprodhom, id_l. |

426 |
rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp. |

427 |
rewrite <- proving_kl3. |

428 |
rewrite -> f_cpr. |

429 |
rewrite -> comp_assoc with (g':=ηv), proving_kl2. |

430 |
rewrite -> cpr_inl. |

431 | |

432 |
assert (aux1: t †' = ([ηv, w]) § ∘ h). |

433 |
rewrite <- proving_unfolding. |

434 |
unfold w, t. |

435 |
rewrite -> comp_assoc, <- proving_kl3. |

436 |
rewrite -> f_cpr. |

437 |
rewrite -> comp_assoc with (f':=inl), -> proving_kl2. |

438 |
rewrite -> cpr_inl. |

439 |
trivial. |

440 |
rewrite <- aux1. |

441 | |

442 | |

443 |
(* right-hand side *) |

444 |
rewrite -> comp_assoc with (h':=out), -> lifting1. |

445 |
rewrite <-2 comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1. |

446 | |

447 |
assert (aux2: (([out ∘ [ηv ∘ inl, ▷t], η ∘ inr ∘ cont (([ηv ∘ inl, ▷t]) §)]) * |

448 |
= ([η ∘ (inl ⊕⊕ cont (([ηv ∘ inl, ▷t]) §)), out ∘ ▷t] * ∘ π))). |

449 |
unfold π. |

450 |
rewrite -> lifting_map. |

451 |
rewrite ->2 f_cpr. |

452 |
rewrite -> cpr_coprodhom. |

453 |
rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl, id_l. |

454 |
rewrite ->2 comp_assoc with (g':=inl), cpr_inl. |

455 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

456 |
rewrite -> comp_assoc with (h':=out), out_unitcofree. |

457 |
rewrite -> comp_assoc;trivial. |

458 |
rewrite <- comp_assoc with (f':=g), -> aux2; clear aux2. |

459 | |

460 |
rewrite <-2 comp_assoc with (g':=π), -> comp_assoc with (f':=π ∘ (out ∘ g)), <- kl3. |

461 |
rewrite -> f_cpr. |

462 |
rewrite -> comp_assoc with (g':=η), kl2. |

463 |
rewrite -> cpr_coprodhom. |

464 |
rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp. |

465 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl. |

466 |
rewrite -> out_unitcofree. |

467 |
rewrite <- proving_kl3. |

468 |
rewrite -> f_cpr. |

469 |
rewrite -> comp_assoc with (f':=inl), proving_kl2. |

470 |
rewrite -> cpr_inl. |

471 |
rewrite <- unfolding_triangle1. |

472 | |

473 | |

474 |
apply f_equal2;trivial. |

475 |
apply f_equal1. |

476 |
apply f_equal2;trivial. |

477 | |

478 | |

479 |
(* left-hand side *) |

480 |
rewrite -> naturality. |

481 |
rewrite -> f_cpr. |

482 |
rewrite -> comp_assoc with (g':=η), map_unit. |

483 |
rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit. |

484 | |

485 |
rewrite -> comp_assoc, <- kl3. |

486 |
rewrite -> f_cpr. |

487 |
rewrite -> comp_assoc with (g':=η), kl2. |

488 |
rewrite -> cpr_inl. |

489 |
rewrite <- f_cpr. |

490 | |

491 |
rewrite -> comp_assoc with (g':=p); unfold p. |

492 |
rewrite -> lifting_map. |

493 |
rewrite -> cpr_coprodhom, -> id_l. |

494 |
rewrite <- comp_assoc with (f':=id ⊕⊕ cont (([ηv ∘ inl, h]) §)), -> cpr_coprodhom, -> id_l. |

495 |
rewrite <- comp_assoc with (f':=cont (([ηv ∘ inl, h]) §)), -> cont_comp. |

496 |
rewrite <- proving_kl3. |

497 |
rewrite -> f_cpr with (f:=([ηv, w]) §). |

498 |
rewrite -> comp_assoc with (g':=ηv), -> proving_kl2, -> cpr_inl. |

499 |
rewrite <- aux1. |

500 | |

501 |
assert (aux3: ([(η ∘ inl) ∘ ([inl, inr ∘ cont (([ηv, t †']) §)]), η ∘ inr]) * |

502 |
∘ η ∘ inl ∘ (id ⊕⊕ cont ([ηv ∘ inl, g] §)) |

503 |
= (η ∘ inl (b:=z)) ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, w]) §)])). |

504 |
rewrite -> kl2. |

505 |
rewrite -> cpr_inl. |

506 |
rewrite <- comp_assoc, -> cpr_coprodhom, -> id_l. |

507 |
rewrite <- comp_assoc with (h':=inr), -> cont_comp. |

508 |
rewrite <- proving_kl3. |

509 |
rewrite -> f_cpr with (f:=([ηv, t †']) §). |

510 |
rewrite -> comp_assoc with (f':=inl), -> proving_kl2. |

511 |
rewrite -> cpr_inl. |

512 |
trivial. |

513 |
rewrite <- aux3; clear aux3. |

514 | |

515 |
rewrite <-2 comp_assoc, <- f_cpr. |

516 | |

517 |
rewrite <- comp_assoc with (h':=η), <- f_cpr. |

518 | |

519 |
assert (aux4: map (([inl, inr ∘ cont (([ηv, t †']) §)]) ⊕⊕ id) = |

520 |
(η ∘ ([inl ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, t †']) §)]), inr (b:=z)])) *). |

521 |
unfold map, coprodhom; rewrite -> id_l. |

522 |
trivial. |

523 |
rewrite <- aux4; clear aux4. |

524 | |

525 |
rewrite <- map_lifting, <- comp_assoc, <- map_naturality. |

526 | |

527 | |

528 |
(* right-hand side *) |

529 |
unfold triangle. |

530 |
rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo); |

531 |
rewrite -> out_tuo_is_id, id_r. |

532 | |

533 |
rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map. |

534 |
rewrite -> cpr_coprodhom, -> id_l. |

535 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl. |

536 |
rewrite -> out_unitcofree. |

537 | |

538 |
apply f_equal2. |

539 |
unfold map; rewrite -> f_cpr. |

540 |
rewrite -> comp_assoc; trivial. |

541 | |

542 |
rewrite -> comp_assoc with (f':=t), -> Hq. |

543 |
unfold q. |

544 |
rewrite -> lifting_map. |

545 |
rewrite -> cpr_coprodhom, -> id_l. |

546 |
rewrite ->4 comp_assoc; trivial. |

547 | |

548 | |

549 | |

550 |
symmetry. |

551 |
apply unfolding_triangle2. |

552 | |

553 |
rewrite -> H_main. |

554 | |

555 |
rewrite -> comp_assoc, <- proving_kl3. |

556 |
rewrite -> f_cpr. |

557 |
rewrite -> comp_assoc with (f':=inl), proving_kl2. |

558 |
rewrite -> cpr_inl. |

559 | |

560 |
rewrite <- unfolding_triangle1. |

561 |
trivial. |

562 |
Qed. |

563 | |

564 | |

565 | |

566 |
(* --- *) |

567 | |

568 |
(* proving codiagonal, split in multiple lemmas/theorems *) |

569 | |

570 |
Definition ξ (x y : Obj) := |

571 |
([inl ⊕⊕ id, inl (b:=x) ∘ inr (a:=y) (b:=x)]). |

572 |
Arguments ξ [x y]. |

573 | |

574 | |

575 |
Lemma ξ1 : forall (x y : Obj), |

576 |
mapc ξ ∘ mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y)) = id. |

577 |
Proof. |

578 |
intros. |

579 |
rewrite -> mapc_comp. |

580 |
unfold ξ. |

581 |
rewrite -> f_cpr. |

582 |
rewrite -> cpr_coprodhom. |

583 |
rewrite -> coprodhom_inl, -> id_l. |

584 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

585 |
rewrite -> coprodhom_inr, -> id_l. |

586 |
rewrite <- f_cpr. |

587 |
rewrite -> inl_inr_is_id, -> id_l. |

588 |
rewrite -> inl_inr_is_id. |

589 |
apply mapc_id. |

590 |
Qed. |

591 | |

592 | |

593 |
Lemma ξ2 : forall (x y : Obj), |

594 |
mapc ([id, inr]) ∘ mapc (ξ (x:=x) (y:=y)) = mapc (a:=a) (b:=b) ([id, inr]). |

595 |
Proof. |

596 |
intros. |

597 |
rewrite -> mapc_comp. |

598 |
unfold ξ. |

599 |
rewrite -> f_cpr. |

600 |
rewrite -> cpr_coprodhom, -> id_l, id_r. |

601 |
rewrite -> inl_inr_is_id. |

602 |
rewrite -> comp_assoc, -> cpr_inl, -> id_r. |

603 |
trivial. |

604 |
Qed. |

605 | |

606 | |

607 | |

608 |
(* A.11 *) |

609 |
Lemma proving_codiagonal_h0 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x))) |

610 |
(h': x ~> (coext T a b (y ⊕ x ⊕ x))), |

611 |
(h' †') †' = ([ηv, (h' †') †']) § ∘ ▷(mapc ([id, inr]) ∘ g') -> |

612 |
(h' †') †' = (mapc ([id, inr]) ∘ g') †'. |

613 | |

614 |
Proof. |

615 |
intros. |

616 | |

617 |
rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ g'). |

618 |
apply unfolding_guarded2. |

619 |
apply guardedtriangle_def. |

620 |
exact H. |

621 | |

622 |
Qed. |

623 | |

624 | |

625 | |

626 |
Theorem proving_codiagonal_clause1 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x))), |

627 |
guarded (mapc ([id, inr]) ∘ g') -> |

628 |
(g' †') †' = ([ηv, (g' †') †']) § ∘ ▷(mapc ([id, inr]) ∘ g'). |

629 | |

630 |
Proof. |

631 |
intros. |

632 |
rewrite <- proving_unfolding at 1. |

633 | |

634 |
assert (aux:([ηv, (g' †') †']) § ∘ g' †' = [ηv, (g' †') †'] § ∘ [ηv, g' †'] § ∘ g'). |

635 |
symmetry; rewrite -> proving_unfolding at 1; trivial. |

636 |
rewrite -> aux at 1; clear aux. |

637 | |

638 |
rewrite -> comp_assoc, <- proving_kl3. |

639 |
rewrite -> f_cpr. |

640 |
rewrite -> proving_kl2. |

641 | |

642 |
rewrite -> proving_unfolding. |

643 | |

644 | |

645 |
rewrite -> guardedtriangle with (f':=mapc ([id, inr]) ∘ g'); trivial. |

646 | |

647 |
rewrite -> comp_assoc, -> liftingcofree_mapc. |

648 |
rewrite -> f_cpr, -> id_l. |

649 |
rewrite -> cpr_inr. |

650 |
trivial. |

651 | |

652 |
Qed. |

653 | |

654 | |

655 | |

656 |
(* A.10 *) |

657 |
Lemma proving_codiagonal_h1 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

658 |
▷(mapc ([id, inr]) ∘ ▷g) = ▷(mapc ([id, inr]) ∘ g). |

659 | |

660 |
Proof. |

661 |
intros. |

662 |
apply out_cong. |

663 |
rewrite ->2 out_triangle. |

664 |
rewrite <-2 comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc. |

665 |
rewrite ->4 comp_assoc, -> map_comp. |

666 |
rewrite -> cpr_coprodhom. |

667 |
rewrite -> f_cpr, -> id_l. |

668 |
rewrite -> cpr_inr. |

669 |
rewrite <- comp_assoc, -> out_triangle. |

670 |
rewrite -> map_naturality. |

671 |
rewrite ->2 comp_assoc, -> map_comp. |

672 |
rewrite <- codiagonal. |

673 |
apply f_equal1. |

674 |
rewrite ->2 comp_assoc, -> map_comp. |

675 |
apply f_equal2;trivial; apply f_equal2;trivial. |

676 |
unfold map. |

677 |
apply f_equal1. |

678 |
rewrite <- comp_assoc; apply f_equal2;trivial. |

679 | |

680 |
case_distinction. |

681 | |

682 |
case_distinction. |

683 |
rewrite ->3 comp_assoc, <- comp_assoc with (h':=([id, inr])), -> coprodhom_inl. |

684 |
rewrite -> comp_assoc, -> cpr_inl. |

685 |
rewrite -> id_r, -> cpr_inl. |

686 |
rewrite -> cpr_inl. |

687 |
trivial. |

688 | |

689 |
rewrite -> coprodhom_inr, -> id_l. |

690 |
rewrite -> cpr_inr. |

691 |
trivial. |

692 | |

693 |
rewrite -> comp_assoc with (f':=inr), -> coprodhom_inl. |

694 |
rewrite ->2 comp_assoc, -> cpr_inl, -> id_r. |

695 |
rewrite -> cpr_inr. |

696 |
trivial. |

697 | |

698 |
Qed. |

699 | |

700 | |

701 | |

702 |
Theorem proving_codiagonal_clause2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

703 |
guarded (mapc ξ ∘ g) -> |

704 |
(g †') †' = ▷(mapc ([id, inr]) ∘ g) †'. |

705 | |

706 |
Proof. |

707 |
intros. |

708 | |

709 |
rewrite <- itercofree_triangle. |

710 |
apply proving_codiagonal_h0. |

711 | |

712 |
rewrite <- proving_codiagonal_h1. |

713 | |

714 |
assert (aux: (g †') †' = (▷g †') †'). |

715 |
rewrite <- itercofree_triangle;trivial. |

716 |
rewrite -> aux; clear aux. |

717 | |

718 |
apply proving_codiagonal_clause1. |

719 | |

720 | |

721 |
unfold guarded in H. |

722 |
inversion H as [u' H']. |

723 | |

724 |
assert (aux1: g = mapc ξ ∘ tuo ∘ map (inl ⊕⊕ id) ∘ u'). |

725 |
rewrite <- comp_assoc, <- H'. |

726 |
rewrite <- comp_assoc with (g':=tuo), -> comp_assoc with (g':=out), -> tuo_out_is_id, -> id_r. |

727 |
rewrite -> comp_assoc, -> ξ1, -> id_r. |

728 |
trivial. |

729 | |

730 | |

731 |
unfold guarded. |

732 | |

733 |
rewrite -> aux1; clear aux1. |

734 |
unfold triangle. |

735 | |

736 |
rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=mapc ξ), |

737 |
-> comp_assoc with (g':=mapc ξ), -> out_mapc. |

738 |
rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=tuo), |

739 |
-> comp_assoc with (f':=map (inl ⊕⊕ id) ∘ u'), -> out_tuo_is_id, -> id_r. |

740 | |

741 |
rewrite -> comp_assoc with (h':=map (ξ ⊕⊕ cont (mapc ξ))), -> map_comp. |

742 |
rewrite -> coprodhom_comp, -> id_l. |

743 | |

744 |
(* |

745 |
assert (aux2: map ((inl ⊕⊕ id) ⊕⊕ id) ∘ π = π ∘ map (ξ (x:=x) (y:=y) ∘ inl |

746 |
⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y))))). |

747 |
unfold π. |

748 |
rewrite ->2 map_comp. |

749 |
rewrite -> cpr_coprodhom. |

750 |
rewrite -> f_cpr. |

751 |
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. |

752 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l. |

753 |
rewrite -> coprodhom_comp, -> id_l. |

754 |
rewrite -> coprodhom_inl. |

755 |
(* is this even true ? see paper *) |

756 |
*) |

757 | |

758 | |

759 |
rewrite -> comp_assoc, -> out_mapc. |

760 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. |

761 | |

762 |
rewrite -> comp_assoc, -> map_comp. |

763 |
rewrite -> coprodhom_comp, -> cpr_inl, -> id_l. |

764 |
rewrite -> map_naturality. |

765 |
rewrite -> comp_assoc; unfold π. |

766 |
rewrite -> comp_assoc, ->2 map_comp. |

767 |
rewrite -> f_cpr. |

768 |
rewrite -> coprodhom_comp. |

769 |
rewrite -> coprodhom_inl, ->2 id_l. |

770 |
rewrite -> comp_assoc, -> coprodhom_inl. |

771 |
rewrite <- comp_assoc, -> coprodhom_inr. |

772 |
rewrite -> cpr_coprodhom. |

773 |
unfold ξ at 1; rewrite -> cpr_inl. |

774 |
rewrite -> coprodhom_comp, -> id_l. |

775 |
rewrite <-2 comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. |

776 |
rewrite -> ξ2. |

777 | |

778 |
exists (map (id ⊕⊕ cont (mapc ([id, inr]))) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ u') †). |

779 | |

780 |
rewrite ->2 map_naturality. |

781 |
apply f_equal1. |

782 |
rewrite ->3 comp_assoc, ->2 map_comp. |

783 |
apply f_equal2; trivial. |

784 |
apply f_equal1. |

785 | |

786 |
rewrite ->2 coprodhom_comp, ->2 id_l, -> id_r. |

787 |
rewrite -> f_cpr. |

788 |
rewrite -> coprodhom_comp. |

789 |
rewrite -> coprodhom_inl, -> id_l. |

790 |
rewrite -> comp_assoc, -> coprodhom_inl. |

791 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

792 |
rewrite -> comp_assoc; trivial. |

793 | |

794 |
Qed. |

795 | |

796 | |

797 | |

798 |
(* A.12 *) |

799 |
Theorem proving_codiagonal_h2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

800 |
guarded g -> |

801 |
▷(g †') = [ηv, g †'] § ∘ mapc ξ ∘ ▷ (mapc ξ ∘ g). |

802 | |

803 |
Proof. |

804 |
intros. |

805 | |

806 |
apply out_cong. |

807 | |

808 |
(* right-hand side *) |

809 |
rewrite ->2 comp_assoc, -> lifting1. |

810 |
unfold triangle at 2. |

811 | |

812 |
rewrite <- comp_assoc with (g':=out), -> out_mapc. |

813 |
rewrite -> comp_assoc with (f':=out), <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), |

814 |
-> out_tuo_is_id, -> id_r. |

815 |
rewrite -> lifting_map. |

816 |
rewrite -> cpr_coprodhom. |

817 |
rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. |

818 |
rewrite -> comp_assoc, -> lifting_map. |

819 |
rewrite -> cpr_coprodhom, -> id_l. |

820 | |

821 |
unfold ξ at 1. |

822 |
rewrite <- comp_assoc with (f':=inl), -> cpr_inl. |

823 |
rewrite <- comp_assoc with (h':=out), -> cpr_coprodhom, -> id_l. |

824 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. |

825 | |

826 |
rewrite -> naturality. |

827 | |

828 |
rewrite ->3 f_cpr. |

829 |
rewrite -> comp_assoc with (h':=out), -> out_unitcofree. |

830 |
rewrite ->5 comp_assoc with (h':=map inl), -> map_unit. |

831 | |

832 |
unfold π. |

833 |
rewrite -> comp_assoc, -> lifting_map. |

834 |
rewrite -> f_cpr. |

835 |
rewrite -> cpr_coprodhom, -> id_l. |

836 |
rewrite -> cpr_inl. |

837 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

838 |
rewrite -> cpr_inr. |

839 | |

840 |
unfold guarded in H. |

841 |
inversion H as [u' H']. |

842 |
rewrite <- comp_assoc with (f':=g), -> H'. |

843 | |

844 |
rewrite -> comp_assoc with (f':=u'), -> map_comp, -> coprodhom_comp, -> id_l. |

845 |
rewrite -> comp_assoc, -> lifting_map. |

846 |
rewrite -> cpr_coprodhom. |

847 |
rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. |

848 | |

849 |
unfold ξ at 1. |

850 |
rewrite -> cpr_inl. |

851 |
rewrite -> cpr_coprodhom, -> id_l. |

852 |
rewrite -> cpr_inl. |

853 |
rewrite <- comp_assoc with (g':=mapc ξ), -> ξ1, -> id_l. |

854 | |

855 | |

856 |
(* left-hand side *) |

857 |
unfold triangle. |

858 |
rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r. |

859 | |

860 |
rewrite -> map_naturality. |

861 |
unfold π. |

862 |
rewrite ->2 comp_assoc, -> map_comp, -> f_cpr. |

863 |
rewrite -> coprodhom_comp, -> coprodhom_inl, -> id_l. |

864 |
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. |

865 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l. |

866 | |

867 |
rewrite <- comp_assoc with (g':=out), <- proving_unfolding at 1. |

868 |
rewrite -> comp_assoc with (h':=out), -> lifting1. |

869 | |

870 |
rewrite -> f_cpr, -> out_unitcofree. |

871 |
rewrite <- comp_assoc with (f':=g), -> H'. |

872 |
rewrite -> comp_assoc with (f':=u'), -> lifting_map. |

873 |
rewrite -> cpr_coprodhom, -> id_l. |

874 |
rewrite -> cpr_inl. |

875 | |

876 |
rewrite -> comp_assoc with (f':=u'), -> map_lifting, -> f_cpr. |

877 |
rewrite ->3 comp_assoc, -> map_unit. |

878 |
rewrite <-2 comp_assoc with (h':=η), -> cpr_inl, -> cpr_inr. |

879 |
unfold coprodhom. |

880 |
rewrite -> f_cpr, -> id_l, ->3 comp_assoc. |

881 | |

882 |
trivial. |

883 |
Qed. |

884 | |

885 | |

886 | |

887 |
Theorem proving_codiagonal_h3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

888 |
guarded g -> |

889 |
(g †') †' = (([ηv ∘ inl, g †']) § ∘ (mapc ξ ∘ g) †') †'. |

890 | |

891 |
Proof. |

892 |
intros. |

893 | |

894 |
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). |

895 |
rewrite -> itercofree_triangle at 1. |

896 |
rewrite -> proving_codiagonal_h2. |

897 | |

898 |
rewrite <- id_l with (f':=ηv). |

899 |
rewrite <- inl_inr_is_id. |

900 |
rewrite -> f_cpr. |

901 | |

902 |
rewrite -> liftingcofree_mapc. |

903 |
unfold ξ at 1. |

904 |
rewrite -> f_cpr. |

905 |
rewrite -> cpr_coprodhom. |

906 |
rewrite -> cpr_inl, -> id_l. |

907 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

908 |
rewrite -> cpr_inr. |

909 | |

910 |
assert (aux1: mapc ([id, inr]) ∘ ([[ηv ∘ inl ∘ inl, mapc inl ∘ g †'], ηv ∘ inr]) § |

911 |
= ([[ηv ∘ inl, g †'], ηv ∘ inr]) §). |

912 |
rewrite -> mapc_liftingcofree. |

913 |
rewrite ->2 f_cpr. |

914 |
rewrite ->2 comp_assoc, -> mapc_unitcofree. |

915 |
rewrite <- comp_assoc with (g':=[id, inr]), -> cpr_inl, -> id_l. |

916 |
rewrite -> comp_assoc with (g':=mapc inl), -> mapc_comp. |

917 |
rewrite -> cpr_inl, -> mapc_id, -> id_r. |

918 |
rewrite -> comp_assoc, -> mapc_unitcofree. |

919 |
rewrite <- comp_assoc, -> cpr_inr. |

920 |
trivial. |

921 |
rewrite <- aux1; clear aux1. |

922 | |

923 |
rewrite -> itercofree_triangle. |

924 |
rewrite <- comp_assoc, <- proving_codiagonal_clause2. |

925 | |

926 |
assert (aux2: mapc inl ∘ ([ηv ∘ inl, g †']) = [(ηv ∘ inl) ∘ inl, mapc (inl (b:=x)) ∘ g †']). |

927 |
rewrite -> f_cpr. |

928 |
rewrite -> comp_assoc, -> mapc_unitcofree. |

929 |
trivial. |

930 |
rewrite <- aux2; clear aux2. |

931 | |

932 |
rewrite -> mapc_unfold at 1. |

933 |
rewrite <- proving_naturality. |

934 | |

935 |
rewrite <- itercofree_triangle. |

936 | |

937 |
trivial. |

938 | |

939 | |

940 |
unfold guarded. |

941 | |

942 | |

943 |
assert (aux4: exists u : x ~> T (y ⊕ a × coext T a b ((y ⊕ x) ⊕ x) ^ b), out∘ ▷(mapc ξ ∘ g) = map (inl ∘ inl ⊕⊕ id) ∘ u). |

944 |
unfold triangle. |

945 |
rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r. |

946 |
rewrite -> comp_assoc, <- comp_assoc with (g':=out), -> out_mapc. |

947 |
rewrite -> comp_assoc; unfold π. |

948 |
rewrite -> map_comp. |

949 |
rewrite -> cpr_coprodhom. |

950 |
unfold ξ. |

951 |
rewrite -> f_cpr. |

952 |
rewrite -> coprodhom_comp, -> id_r. |

953 |
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl, <- comp_assoc with (g':=out). |

954 | |

955 |
unfold guarded in H. |

956 |
inversion H as [z Q]. |

957 |
rewrite -> Q. |

958 |
rewrite -> comp_assoc, -> map_comp. |

959 |
rewrite -> cpr_coprodhom, -> id_l. |

960 |
rewrite -> cpr_inl. |

961 |
unfold coprodhom at 2; rewrite -> id_l. |

962 | |

963 |
assert (aux5: z = π ∘ π ∘ z). |

964 |
unfold π. |

965 |
rewrite -> map_comp. |

966 |
unfold coprodhom. |

967 |
coprod_simp. |

968 |
rewrite ->2 id_l. |

969 |
rewrite <- f_cpr. |

970 |
rewrite -> inl_inr_is_id, -> id_l. |

971 |
rewrite -> inl_inr_is_id, -> map_id, -> id_r; trivial. |

972 |
rewrite -> aux5; clear aux5. |

973 | |

974 |
rewrite <- comp_assoc with (g':=π), -> comp_assoc with (g':=π); |

975 |
unfold π at 1. |

976 |
rewrite -> map_comp. |

977 |
rewrite -> f_cpr. |

978 |
rewrite -> cpr_coprodhom, -> cpr_inl, -> id_l. |

979 |
rewrite -> comp_assoc with (g':=inl) (f':=inr), -> cpr_inl. |

980 |
rewrite -> cpr_inr, <- comp_assoc with (h':=inl) (g':=inr). |

981 |
rewrite <- f_cpr. |

982 |
unfold map at 2. |

983 |
rewrite -> f_cpr with (f:=η). |

984 |
rewrite <- map_unit. |

985 |
rewrite <- map_comp, <- comp_assoc with (h':=map inl). |

986 | |

987 | |

988 |
rewrite <- naturality. |

989 | |

990 |
rewrite -> comp_assoc, -> map_lifting. |

991 |
rewrite -> comp_assoc, -> map_comp. |

992 |
unfold coprodhom at 1. |

993 |
rewrite -> f_cpr. |

994 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

995 |
rewrite -> comp_assoc with (g':=inr), -> cpr_inr, -> id_l. |

996 |
rewrite <- comp_assoc with (g':=inl), <- map_lifting. |

997 |
rewrite -> kl1, -> id_l. |

998 | |

999 |
exists (map (id ⊕⊕ cont (mapc ([inl ⊕⊕ id, inl ∘ inr]))) ∘ (π ∘ z) †). |

1000 | |

1001 |
rewrite ->2 comp_assoc, -> map_comp. |

1002 |
unfold coprodhom. |

1003 |
coprod_simp. |

1004 |
rewrite ->3 id_l, -> comp_assoc. |

1005 |
trivial. |

1006 | |

1007 | |

1008 |
inversion aux4 as [w H']. |

1009 | |

1010 |
rewrite -> comp_assoc with (h':=mapc ξ). |

1011 |
rewrite -> mapc_liftingcofree. |

1012 |
rewrite ->2 f_cpr. |

1013 |
rewrite ->4 comp_assoc with (h':=mapc ξ), -> mapc_unitcofree, -> mapc_comp. |

1014 |
rewrite <-2 comp_assoc with (g':=ξ). |

1015 |
unfold ξ at 1 2 3. |

1016 |
rewrite -> cpr_inl, -> cpr_inr. |

1017 |
rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl. |

1018 |
rewrite -> comp_assoc, -> lifting1. |

1019 |
rewrite ->2 f_cpr. |

1020 |
rewrite <- comp_assoc with (g':=out), -> H'. |

1021 |
rewrite -> comp_assoc, -> lifting_map. |

1022 |
rewrite -> cpr_coprodhom, -> id_l. |

1023 |
rewrite -> comp_assoc with (g':=inl), ->2 cpr_inl. |

1024 |
rewrite -> comp_assoc with (h':=out), -> out_unitcofree. |

1025 |
rewrite -> comp_assoc. |

1026 |
rewrite <- cpr_coprodhom with (f:=(η ∘ inl) ∘ inl) (i:=cont |

1027 |
(([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'], ηv ∘ (inl ∘ inr)]) §)). |

1028 |
rewrite <- comp_assoc, <- f_cpr. |

1029 |
rewrite <- map_unit. |

1030 |
rewrite <- comp_assoc with (g':=η). |

1031 |
rewrite <- map_lifting. |

1032 |
rewrite <- comp_assoc with (h':=map ([inl ∘ inl, inr])). |

1033 |
exists ((η ∘ (inl ⊕⊕ cont (([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'], |

1034 |
ηv ∘ (inl ∘ inr)]) §))) * ∘ w). |

1035 |
unfold coprodhom at 3. |

1036 |
rewrite -> id_l. |

1037 |
trivial. |

1038 | |

1039 | |

1040 |
exact H. |

1041 | |

1042 |
Qed. |

1043 | |

1044 | |

1045 | |

1046 |
Theorem proving_codiagonal_h4 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

1047 |
guarded g -> |

1048 |
((mapc ξ ∘ g) †') †' = (g †') †'. |

1049 | |

1050 |
Proof. |

1051 |
intros. |

1052 | |

1053 |
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). |

1054 | |

1055 | |

1056 |
symmetry. |

1057 |
apply unfolding_guarded2. |

1058 | |

1059 |
unfold guarded. |

1060 |
unfold guarded in H. |

1061 |
inversion H as [u' H']. |

1062 | |

1063 |
exists (map (id ⊕⊕ cont ([ηv,( mapc ξ ∘ g) †'] §) ) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ map (id ⊕⊕ cont (mapc ξ)) ∘ u') †). |

1064 |
rewrite -> out_itercofree. |

1065 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. |

1066 |
rewrite <- comp_assoc with (g':=out), -> H'. |

1067 |
rewrite -> naturality. |

1068 |
rewrite -> map_naturality. |

1069 |
rewrite -> map_naturality. |

1070 |
apply f_equal1. |

1071 |
unfold π. |

1072 |
rewrite -> comp_assoc, -> lifting_map. |

1073 |
rewrite -> comp_assoc, -> lifting_map. |

1074 |
rewrite -> comp_assoc, -> lifting_map. |

1075 |
rewrite -> comp_assoc, -> map_comp. |

1076 |
rewrite ->2 comp_assoc, ->2 map_comp. |

1077 |
apply f_equal2; trivial. |

1078 |
rewrite -> f_cpr. |

1079 |
rewrite ->3 cpr_coprodhom. |

1080 |
rewrite -> id_l. |

1081 |
rewrite ->2 coprodhom_comp. |

1082 |
rewrite ->2 id_l, ->2 id_r. |

1083 |
rewrite -> f_cpr with (f:=(inl ⊕⊕ cont (([ηv, (mapc ξ ∘ g) †']) §)) ⊕⊕ id). |

1084 |
rewrite -> cpr_coprodhom. |

1085 |
rewrite -> id_l. |

1086 |
unfold map. |

1087 |
apply f_equal1. |

1088 |
case_distinction. |

1089 |
rewrite <- comp_assoc with (f':=inl). |

1090 |
rewrite -> cpr_inl. |

1091 |
rewrite -> coprodhom_comp. |

1092 |
rewrite -> coprodhom_inl. |

1093 |
unfold ξ. |

1094 |
rewrite -> cpr_inl. |

1095 |
rewrite -> cpr_coprodhom. |

1096 |
rewrite -> comp_assoc, -> kl2. |

1097 |
unfold coprodhom. |

1098 |
rewrite -> f_cpr. |

1099 |
rewrite ->3 id_l. |

1100 |
rewrite ->2 comp_assoc. |

1101 |
trivial. |

1102 |
rewrite <- comp_assoc with (f':=inr). |

1103 |
rewrite ->2 cpr_inr. |

1104 |
rewrite -> comp_assoc with (g':=inl), -> cpr_inl. |

1105 |
rewrite <- comp_assoc with (f':=inr). |

1106 |
rewrite -> cpr_inr. |

1107 |
rewrite ->2 comp_assoc, -> kl2. |

1108 |
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. |

1109 |
rewrite <-2 comp_assoc with (f':=inr). |

1110 |
rewrite -> coprodhom_inr. |

1111 |
rewrite ->4 comp_assoc. |

1112 |
trivial. (* this might be possible in a much simpler way *) |

1113 | |

1114 | |

1115 |
rewrite -> proving_codiagonal_h3 at 1. |

1116 | |

1117 |
rewrite <- proving_unfolding at 1. |

1118 | |

1119 |
rewrite <- proving_codiagonal_h3. |

1120 | |

1121 |
rewrite -> comp_assoc, <- proving_kl3. |

1122 |
rewrite -> f_cpr. |

1123 |
rewrite -> comp_assoc, -> proving_kl2. |

1124 |
rewrite -> cpr_inl. |

1125 | |

1126 |
rewrite -> proving_unfolding. |

1127 |
trivial. |

1128 | |

1129 |
exact H. |

1130 |
exact H. |

1131 |
Qed. |

1132 | |

1133 | |

1134 | |

1135 |
Theorem proving_codiagonal_clause3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

1136 |
guarded g -> |

1137 |
(mapc ([id, inr]) ∘ g) †' = (g †') †'. |

1138 | |

1139 |
Proof. |

1140 |
intros. |

1141 | |

1142 |
set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). |

1143 | |

1144 |
transitivity (((mapc ξ ∘ g) †') †'). |

1145 | |

1146 |
rewrite -> proving_codiagonal_clause2. |

1147 |
rewrite <- itercofree_triangle. |

1148 |
rewrite -> comp_assoc, -> ξ2. |

1149 |
trivial. |

1150 | |

1151 |
unfold guarded. |

1152 |
rewrite -> comp_assoc with (f':=g), -> ξ1, -> id_r. |

1153 |
exact H. |

1154 | |

1155 | |

1156 |
apply proving_codiagonal_h4. |

1157 |
apply H. |

1158 | |

1159 |
Qed. |

1160 | |

1161 | |

1162 | |

1163 |
Theorem proving_codiagonal : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), |

1164 |
((ηv ∘ ([id, inr])) § ∘ g) †' = (g †') †'. |

1165 | |

1166 |
Proof. |

1167 |
intros. |

1168 |
rewrite <- mapc_unfold. |

1169 | |

1170 |
(* clause 4 *) |

1171 | |

1172 |
set (h:= mapc ξ ∘ ▷ g). |

1173 | |

1174 | |

1175 |
transitivity (((mapc ξ ∘ h) †') †'). |

1176 | |

1177 |
rewrite <- proving_codiagonal_clause3. |

1178 | |

1179 |
rewrite -> comp_assoc, ξ2. |

1180 | |

1181 |
unfold h. |

1182 | |

1183 |
rewrite -> comp_assoc, ξ2. |

1184 | |

1185 |
rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ ▷g). |

1186 | |

1187 |
rewrite -> proving_codiagonal_h1. |

1188 | |

1189 |
apply itercofree_triangle. |

1190 | |

1191 |
unfold h. |

1192 |
rewrite -> comp_assoc, -> ξ1, -> id_r. |

1193 |
apply guardedtriangle_def. |

1194 | |

1195 | |

1196 |
unfold h. |

1197 | |

1198 |
rewrite -> comp_assoc, -> ξ1, -> id_r. |

1199 |
rewrite <- itercofree_triangle. |

1200 |
trivial. |

1201 | |

1202 |
Qed. |

1203 | |

1204 | |

1205 | |

1206 |
(* --- *) |

1207 | |

1208 | |

1209 | |

1210 |
Theorem proving_uniformity_guarded : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x), |

1211 |
guarded g -> |

1212 |
f ∘ h = mapc (id ⊕⊕ h) ∘ g -> |

1213 |
f †' ∘ h = g †'. |

1214 | |

1215 |
Proof. |

1216 |
intros. |

1217 | |

1218 |
apply unfolding_guarded2. |

1219 |
apply H. |

1220 | |

1221 |
assert (aux: ([ηv, f †' ∘ h]) § = ([ηv, f †']) § ∘ mapc (id ⊕⊕ h)). |

1222 |
rewrite -> liftingcofree_mapc. |

1223 |
rewrite -> cpr_coprodhom, id_l; trivial. |

1224 |
rewrite -> aux. |

1225 | |

1226 |
rewrite <- comp_assoc, <- H0. |

1227 |
rewrite -> comp_assoc, -> proving_unfolding. |

1228 |
trivial. |

1229 |
Qed. |

1230 | |

1231 | |

1232 | |

1233 |
Theorem proving_uniformity : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x), |

1234 |
f ∘ h = (ηv ∘ (id ⊕⊕ h)) § ∘ g -> |

1235 |
f †' ∘ h = g †'. |

1236 | |

1237 |
Proof. |

1238 |
intros. |

1239 |
rewrite <- mapc_unfold in H. |

1240 | |

1241 |
assert (H1: (π ∘ out ∘ f) † ∘ h = |

1242 |
map (id ⊕⊕ cont (mapc (id ⊕⊕ h))) ∘ (π ∘ out ∘ g) †). |

1243 | |

1244 |
rewrite -> map_naturality. |

1245 | |

1246 |
apply uniformity. |

1247 | |

1248 |
rewrite <- comp_assoc, -> H. |

1249 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. |

1250 | |

1251 |
rewrite <-2 comp_assoc with (f':=g), ->3 comp_assoc with (f':=out ∘ g); |

1252 |
apply f_equal2;trivial. |

1253 | |

1254 |
unfold π. |

1255 |
rewrite ->3 map_comp. |

1256 |
apply f_equal1. |

1257 |
rewrite -> cpr_coprodhom. |

1258 |
rewrite -> coprodhom_comp, -> id_l, -> id_r. |

1259 |
rewrite -> f_cpr. |

1260 |
rewrite -> coprodhom_comp, -> id_l. |

1261 |
rewrite -> coprodhom_inl, -> id_l. |

1262 |
rewrite -> comp_assoc, -> coprodhom_inl. |

1263 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

1264 |
rewrite -> f_cpr. |

1265 |
rewrite -> coprodhom_comp, -> id_l, -> id_r. |

1266 |
rewrite -> comp_assoc, -> coprodhom_inl, -> id_l. |

1267 |
rewrite -> comp_assoc; trivial. |

1268 | |

1269 | |

1270 |
assert (H2: (▷f) ∘ h = mapc (id ⊕⊕ h) ∘ ▷g). |

1271 |
unfold triangle. |

1272 |
rewrite <- comp_assoc, -> H1. |

1273 |
rewrite ->2 comp_assoc; apply f_equal2; trivial. |

1274 |
apply out_cong. |

1275 |
rewrite -> comp_assoc with (g':=mapc (id ⊕⊕ h)), -> out_mapc. |

1276 |
rewrite ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. |

1277 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo), -> out_tuo_is_id, -> id_r. |

1278 |
rewrite ->2 map_comp. |

1279 |
rewrite ->2 coprodhom_comp, -> id_l. |

1280 |
rewrite -> coprodhom_inl. |

1281 |
rewrite ->2 id_l, -> id_r; trivial. |

1282 | |

1283 |
rewrite -> itercofree_triangle. |

1284 |
symmetry; rewrite -> itercofree_triangle; symmetry. |

1285 | |

1286 |
apply proving_uniformity_guarded. |

1287 | |

1288 |
apply guardedtriangle_def. |

1289 | |

1290 |
apply H2. |

1291 | |

1292 |
Qed. |

1293 | |

1294 | |

1295 | |

1296 |
(* --- *) |

1297 | |

1298 | |

1299 | |

1300 |
Theorem proving_str1 : forall |

1301 |
(x : Obj), |

1302 |
pr2 (a:=terminal_obj) (b:=coext T a b x) = (ηv ∘ pr2) § ∘ τv. |

1303 | |

1304 |
Proof. |

1305 |
intros. |

1306 |
rewrite <- mapc_unfold. |

1307 | |

1308 |
assert (H1: pr2 (a:=terminal_obj) (b:=coext T a b x) = mapc pr2 ∘ (mapc (pair bang id) ∘ pr2)). |

1309 |
rewrite -> comp_assoc, -> mapc_comp. |

1310 |
rewrite -> pr2_pair. |

1311 |
rewrite -> mapc_id, -> id_r. |

1312 |
trivial. |

1313 | |

1314 |
rewrite -> H1. |

1315 |
apply f_equal2;trivial. |

1316 | |

1317 | |

1318 |
apply strength2. |

1319 | |

1320 |
assert (H2: id (a:=terminal_obj × x) = (pair bang id) ∘ pr2). |

1321 |
rewrite -> pair_f, -> id_r. |

1322 | |

1323 |
assert (aux1: bang ∘ pr2 (a:=terminal_obj) (b:=x) = pr1). |

1324 |
transitivity (bang (a:=terminal_obj × x)). |

1325 |
apply bang_axiom. |

1326 |
symmetry; apply bang_axiom. |

1327 |
rewrite -> aux1; clear aux1. |

1328 |
symmetry; apply pr1_pr2_is_id. |

1329 | |

1330 |
rewrite -> H2. |

1331 | |

1332 | |

1333 |
rewrite -> map_comp. |

1334 |
assert (aux2: ((pair bang id) ∘ pr2 (a:=terminal_obj) (b:=x) ⊕⊕ cont (mapc (pair bang id) ∘ pr2)) ∘ δ = |

1335 |
((pair bang id) ⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (pair bang id (a:=x)))) ∘ pr2). |

1336 |
set (y:=(pair bang id)). |

1337 |
rewrite <-2 pr2_prodhom with (f:=id). |

1338 |
rewrite <- cont_comp. |

1339 |
rewrite <- coprodhom_comp. |

1340 |
rewrite <- comp_assoc, -> delta. |

1341 |
unfold δ. |

1342 |
rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l. |

1343 |
unfold cont at 1. |

1344 |
rewrite -> prodhom_pair, -> id_r. |

1345 |
rewrite -> curry2. |

1346 |
rewrite -> pr2_pair. |

1347 |
rewrite -> curry_uncurry. |

1348 |
rewrite <- pair_f. |

1349 |
rewrite -> pr1_pr2_is_id, -> id_r. |

1350 |
unfold dist2. |

1351 |
rewrite -> comp_assoc, <- uncurry2. |

1352 |
rewrite -> f_cpr. |

1353 |
rewrite ->2 curry2. |

1354 |
rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. |

1355 |
rewrite -> comp_assoc with (g':=inr), -> coprodhom_inr. |

1356 |
rewrite <-2 comp_assoc with (g':=pr2). |

1357 |
rewrite <- comp_assoc, -> swap_prodhom. |

1358 |
rewrite -> comp_assoc, <- uncurry1. |

1359 |
rewrite -> cpr_coprodhom. |

1360 |
rewrite ->2 curry1. |

1361 |
rewrite <-2 comp_assoc with (f':=y ×× id), -> swap_prodhom. |

1362 |
rewrite -> comp_assoc with (g':=id ×× y), -> pr2_prodhom. |

1363 |
rewrite <-2 comp_assoc with (f':=cont (mapc y) ×× id), -> swap_prodhom. |

1364 |
rewrite -> comp_assoc with (g':=id ×× cont (mapc y)), -> pr2_prodhom. |

1365 |
rewrite <-2 comp_assoc with (f':=swapp); unfold swapp. |

1366 |
rewrite ->2 pr2_pair. |

1367 |
rewrite ->2 comp_assoc, -> curry_cpr_pr1. |

1368 |
rewrite <- comp_assoc, -> pr1_pair. |

1369 |
trivial. |

1370 |
rewrite -> aux2; clear aux2. |

1371 | |

1372 |
rewrite <- comp_assoc, <- map_comp. |

1373 |
rewrite <- comp_assoc, -> comp_assoc with (g':=τ). |

1374 |
rewrite <- str1. |

1375 |
rewrite -> pr2_prodhom. |

1376 |
rewrite -> comp_assoc, -> out_mapc. |

1377 |
rewrite -> comp_assoc; trivial. |

1378 | |

1379 |
Qed. |

1380 | |

1381 | |

1382 | |

1383 |
Theorem proving_str2 : forall |

1384 |
(x y z : Obj), |

1385 |
(ηv ∘ p_assoc1) § ∘ τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) = |

1386 |
τv ∘ (id ×× τv) ∘ p_assoc1. |

1387 | |

1388 |
Proof. |

1389 |
intros. |

1390 |
rewrite <- mapc_unfold. |

1391 | |

1392 |
assert (H_main: τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) |

1393 |
= mapc p_assoc2 ∘ (τv ∘ (id ×× τv)) ∘ p_assoc1). |

1394 |
symmetry. |

1395 |
apply strength2. |

1396 |
rewrite ->2 comp_assoc, -> out_mapc. |

1397 |
rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> strength1. |

1398 |
rewrite <- comp_assoc with (f':=id ×× τv), -> prodhom_comp, -> id_l. |

1399 |
rewrite -> strength1. |

1400 |
rewrite ->3 comp_assoc, -> map_comp. |

1401 |
rewrite -> coprodhom_comp, -> id_l, -> cont_comp. |

1402 | |

1403 |
rewrite <- comp_assoc with (g':=τ). |

1404 |
assert (aux1: map (id ×× (((id ⊕⊕ cont τv) ∘ δ))) ∘ τ ∘ (id ×× (τ ∘ (id ×× out))) |

1405 |
= (τ ∘ (id (a:=x) ×× ((map (id ⊕⊕ cont τv) ∘ map δ) ∘ τ) ∘ (id (a:=y) ×× out (x:=z) (a:=a) (b:=b))))). |

1406 |
rewrite -> map_comp. |

1407 |
rewrite <- id_l with (f':=id), <-2 comp_assoc. |

1408 |
rewrite <- prodhom_comp with (h:=map ((id ⊕⊕ cont τv) ∘ δ)). |

1409 |
rewrite ->2 comp_assoc, <- str_map. |

1410 |
rewrite -> id_l; trivial. |

1411 |
rewrite <- aux1; clear aux1. |

1412 | |

1413 |
rewrite <-6 comp_assoc. |

1414 |
assert (aux2: map p_assoc1 ∘ τ ∘ (id ×× out) = τ ∘ ((id ×× τ ∘ (id ×× out (x:=z) (a:=a) (b:=b))) ∘ p_assoc1 (a:=x) (b:=y))). |

1415 |
rewrite -> str2. |

1416 |
unfold p_assoc1. |

1417 |
rewrite <- comp_assoc with (g':=id ×× τ), -> prodhom_pair, -> id_r. |

1418 |
rewrite -> prodhom_pair, -> id_r. |

1419 |
rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_pair, -> id_r. |

1420 |
rewrite <- comp_assoc, -> pair_f. |

1421 |
rewrite <- comp_assoc, -> pr1_prodhom, -> id_r. |

1422 |
rewrite <- comp_assoc, -> pair_f. |

1423 |
rewrite <- comp_assoc, -> pr1_prodhom, -> id_r. |

1424 |
rewrite -> pr2_prodhom. |

1425 |
trivial. |

1426 |
rewrite <- aux2; clear aux2. |

1427 | |

1428 |
rewrite -> comp_assoc, -> map_comp. |

1429 |
rewrite -> comp_assoc, -> map_comp. |

1430 |
rewrite ->2 comp_assoc, -> map_comp. |

1431 |
rewrite <- comp_assoc with (g':=δ), <-3 comp_assoc with (f':=p_assoc1). |

1432 | |

1433 |
assert (aux3: (p_assoc1 ⊕⊕ (id ×× ((id ×× τv) ∘ p_assoc1) ^^ id)) ∘ δ |

1434 |
= δ ∘ ((id ×× (id ⊕⊕ cont (τv (y:=z) (a:=a) (b:=b))) ∘ δ (a:=a) (b:=b) (y:=z)) ∘ p_assoc1 (a:=x) (b:=y))). |

1435 |
rewrite -> comp_assoc. |

1436 |
symmetry. |

1437 |
rewrite <- id_l with (f':=id). |

1438 |
rewrite <- prodhom_comp. |

1439 |
rewrite -> comp_assoc. |

1440 |
rewrite <- delta. |

1441 |
rewrite -> prodhom_id. |

1442 |
rewrite <-2 comp_assoc, <- p_assoc_delta. |

1443 |
rewrite -> comp_assoc, -> coprodhom_comp, -> id_r. |

1444 |
rewrite -> cont_comp, -> id_l. |

1445 |
unfold cont. |

1446 |
trivial. |

1447 |
rewrite <- aux3; clear aux3. |

1448 | |

1449 |
rewrite ->3 comp_assoc, -> coprodhom_comp. |

1450 |
rewrite -> p_assoc_id2. |

1451 |
unfold cont. |

1452 |
rewrite -> prodhom_comp, -> id_l. |

1453 |
rewrite -> post_comp_comp. |

1454 |
rewrite -> map_comp. |

1455 |
rewrite ->3 comp_assoc;trivial. |

1456 | |

1457 |
rewrite -> H_main. |

1458 |
rewrite ->2 comp_assoc, -> mapc_comp. |

1459 |
rewrite -> p_assoc_id1. |

1460 |
rewrite -> mapc_id, -> id_r. |

1461 |
trivial. |

1462 |
Qed. |

1463 | |

1464 | |

1465 | |

1466 |
Theorem proving_str3 :forall (x y : Obj), |

1467 |
τv (x:=x) (y:=y) (a:=a) (b:=b) ∘ (id ×× ηv) = ηv. |

1468 | |

1469 |
Proof. |

1470 |
intros. |

1471 |
symmetry. |

1472 |
unfold ηv at 1. |

1473 |
apply out_cong. |

1474 |
rewrite ->2 comp_assoc; rewrite -> out_tuo_is_id; rewrite -> id_r. |

1475 |
rewrite -> comp_assoc; rewrite -> strength1. |

1476 | |

1477 |
assert (aux: τ ∘ ((id ×× out) ∘ (id (a:=x) ×× ηv (a:=a) (b:=b) (x:=y))) = η ∘ (id ×× inl)). |

1478 |
rewrite -> prodhom_comp; rewrite -> id_l; rewrite -> out_unitcofree. |

1479 |
rewrite <- id_r with (f':=id) at 1; rewrite <- prodhom_comp with (g:=id); rewrite -> comp_assoc. |

1480 |
rewrite -> str3. |

1481 |
trivial. |

1482 |
rewrite <- comp_assoc with (f':=id ×× ηv); rewrite <- comp_assoc with (g':=τ); rewrite -> aux; clear aux. |

1483 | |

1484 |
rewrite <- map_unit with (f:=id ×× inl). |

1485 |
rewrite -> comp_assoc; rewrite <- comp_assoc with (g':=map δ); rewrite -> map_comp. |

1486 |
unfold δ. |

1487 |
rewrite <- comp_assoc with (g':=dist2), -> dist2_inl. |

1488 |
rewrite -> coprodhom_inl, -> id_l. |

1489 |
rewrite -> map_comp; rewrite -> coprodhom_inl; rewrite -> id_l. |

1490 |
rewrite -> map_unit; trivial. |

1491 | |

1492 |
Qed. |

1493 | |

1494 | |

1495 | |

1496 |
Theorem proving_str4 : forall x y z (f: x ~> (coext T a b y)), |

1497 |
(τv ∘ (id ×× f)) § ∘ τv = τv ∘ (id (a:=z) ×× f §). |

1498 | |

1499 |
Proof. |

1500 |
intros. |

1501 | |

1502 |
set (g:=[f,ηv]). |

1503 | |

1504 |
assert (H1: id = g § ∘ mapc inr). |

1505 |
unfold g. |

1506 |
rewrite -> liftingcofree_mapc. |

1507 |
rewrite -> cpr_inr. |

1508 |
rewrite -> proving_kl1. |

1509 |
trivial. |

1510 | |

1511 |
assert (H2: f = g ∘ inl). |

1512 |
unfold g; rewrite -> cpr_inl; trivial. |

1513 | |

1514 | |

1515 |
assert (H_main: (τv ∘ (id ×× g)) § ∘ τv = τv ∘ (id (a:=z) ×× g §)). |

1516 | |

1517 |
transitivity (coit ((map δ) ∘ τ ∘ (id (a:=z) ×× [map (id ⊕⊕ cont (mapc inr)) ∘ out ∘ g, η ∘ inr]* ∘ out))). |

1518 | |

1519 |
apply coit2. |

1520 | |

1521 |
set (h:=map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out ∘ g). |

1522 | |

1523 |
assert (aux1: [(map δ) ∘ τ ∘ (id ×× h), η ∘ inr] * ∘ (map δ) = (map δ) ∘ (τ ∘ (id (a:=z) ×× [h, η ∘ inr]))*). |

1524 |
unfold δ at 2. |

1525 |
rewrite -> lifting_map. |

1526 |
rewrite -> comp_assoc. |

1527 |
rewrite -> cpr_coprodhom. |

1528 |
rewrite -> id_l. |

1529 | |

1530 |
rewrite -> map_lifting. |

1531 |
apply f_equal1. |

1532 | |

1533 |
assert (aux2: η ∘ δ ∘ (id ×× inr (a:=y)) = |

1534 |
(η ∘ inr) ∘ (pair (pr1 ∘ pr2) (curry (pair (pr1 ∘ pr1) |

1535 |
(uncurry (b:=b) (c:=coext T a b (x ⊕ y)) (pr2 (a:=a) ∘ pr2 (a:=z))))))). |

1536 |
unfold δ. |

1537 |
rewrite <-2 comp_assoc, -> dist2_inr. |

1538 |
rewrite -> coprodhom_inr. |

1539 |
rewrite <- comp_assoc; trivial. |

1540 |
rewrite <- aux2; clear aux2. |

1541 | |

1542 |
rewrite <- map_unit. |

1543 |
rewrite <- str3. |

1544 |
rewrite <-2 comp_assoc with (f':=id ×× inr). |

1545 |
rewrite -> prodhom_comp, -> id_l. |

1546 |
unfold dist2. |

1547 |
rewrite -> comp_assoc, <- uncurry2. |

1548 |
rewrite -> f_cpr. |

1549 |
rewrite ->2 curry2. |

1550 |
rewrite -> comp_assoc, -> cpr_inl. |

1551 |
rewrite -> comp_assoc, -> cpr_inr. |

1552 |
apply swapp_switch. |

1553 |
apply curry_cong. |

1554 |
rewrite -> curry_uncurry. |

1555 |
case_distinction. |

1556 |
rewrite -> cpr_inl. |

1557 |
rewrite -> curry1. |

1558 |
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. |

1559 |
rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inl), -> prodhom_comp. |

1560 |
rewrite -> cpr_inl, -> id_l. |

1561 |
rewrite -> comp_assoc; trivial. |

1562 |
rewrite -> cpr_inr. |

1563 |
rewrite -> curry1. |

1564 |
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. |

1565 |
rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inr), -> prodhom_comp. |

1566 |
rewrite -> cpr_inr, -> id_l. |

1567 |
rewrite -> comp_assoc; trivial. |

1568 | |

1569 |
rewrite <- comp_assoc with (g':=τ). |

1570 |
assert (aux3: (τ ∘ (id ×× [h, η ∘ inr])) * ∘ τ ∘ (id ×× out) = τ ∘ (id (a:=z) ×× ([h, η ∘ inr]) * ∘ out)). |

1571 |
rewrite -> str4. |

1572 |
rewrite <- comp_assoc. |

1573 |
rewrite -> prodhom_comp. |

1574 |
rewrite -> id_l; trivial. |

1575 |
rewrite <- aux3; clear aux3. |

1576 | |

1577 |
rewrite ->2 comp_assoc with (h':=map δ). |

1578 |
rewrite <- aux1; clear aux1. |

1579 | |

1580 |
unfold h. |

1581 |
rewrite <- comp_assoc with (h':=map δ). |

1582 |
assert (aux4: (id ×× (map (id ⊕⊕ cont (mapc inr)))) ∘ (id ×× (out ∘ g)) = id (a:=z) ×× (map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out) ∘ g). |

1583 |
rewrite -> prodhom_comp, -> id_l. |

1584 |
rewrite -> comp_assoc; trivial. |

1585 |
rewrite <- aux4; clear aux4. |

1586 | |

1587 |
rewrite -> comp_assoc with (h':=τ), <- str_map. |

1588 |
rewrite ->2 comp_assoc with (h':=map δ), -> map_comp. |

1589 |
rewrite <- delta. |

1590 |
rewrite -> prodhom_id. |

1591 |
rewrite ->4 comp_assoc, -> map_lifting. |

1592 |
rewrite -> f_cpr. |

1593 |
rewrite ->2 comp_assoc, -> map_comp. |

1594 |
rewrite -> comp_assoc with (g':=η), -> map_unit. |

1595 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

1596 | |

1597 |
assert (aux5: (id ⊕⊕ cont ((τv ∘ (id ×× (g ∘ inr))) § ∘ τv)) = (id ⊕⊕ cont ((τv ∘ (id ×× g)) § ∘ τv)) ∘ ((id (a:=(z × y)) ⊕⊕ cont (a:=a) (b:=b) (id (a:=z) ×× mapc inr)))). |

1598 |
rewrite -> coprodhom_comp, -> id_l, -> cont_comp. |

1599 |
rewrite <- comp_assoc, -> naturality_τv. |

1600 |
rewrite -> comp_assoc, -> liftingcofree_mapc. |

1601 |
rewrite <- comp_assoc, -> prodhom_comp, -> id_l. |

1602 |
trivial. |

1603 |
rewrite ->2 comp_assoc. |

1604 |
rewrite <- aux5; clear aux5. |

1605 | |

1606 |
symmetry; unfold g at 1; symmetry. |

1607 |
rewrite -> cpr_inr. |

1608 |
rewrite -> proving_str3. |

1609 |
rewrite -> proving_kl1, -> id_r. |

1610 | |

1611 |
rewrite -> lifting1. |

1612 |
rewrite <- comp_assoc, -> strength1. |

1613 |
rewrite ->3 comp_assoc, -> lifting_map. |

1614 |
rewrite -> cpr_coprodhom, -> id_l. |

1615 |
rewrite -> comp_assoc, -> strength1. |

1616 |
rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_comp, -> id_l. |

1617 |
rewrite -> map_comp. |

1618 |
rewrite <- comp_assoc with (f':=cont τv), -> cont_comp. |

1619 |
trivial. |

1620 | |

1621 | |

1622 | |

1623 |
unfold τv. |

1624 |
apply fusion. |

1625 |
rewrite ->2 comp_assoc, -> map_comp. |

1626 |
rewrite <- comp_assoc with (f':=(id ×× g §)), -> prodhom_comp, -> id_l. |

1627 |
rewrite -> lifting1. |

1628 |
rewrite <- prodhom_id. |

1629 |
rewrite -> delta. |

1630 |
rewrite <-2 comp_assoc with (g':=τ). |

1631 | |

1632 |
assert (aux6: id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) * ∘ out = |

1633 |
(id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) *) ∘ (id (a:=z) ×× out)). |

1634 |
rewrite -> prodhom_comp, -> id_l. |

1635 |
trivial. |

1636 |
rewrite -> aux6; clear aux6. |

1637 | |

1638 |
assert (aux7: id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) * ∘ out = |

1639 |
(id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) *) ∘ (id (a:=z) ×× out)). |

1640 |
rewrite -> prodhom_comp, -> id_l. |

1641 |
trivial. |

1642 |
rewrite -> aux7; clear aux7. |

1643 | |

1644 |
rewrite ->2 comp_assoc with (h':=τ), <-2 str4. |

1645 |
rewrite ->4 comp_assoc; |

1646 |
apply f_equal2;trivial. |

1647 |
apply f_equal2;trivial. |

1648 |
rewrite ->2 map_lifting. |

1649 |
apply f_equal1. |

1650 |
rewrite <- map_comp, <- comp_assoc with (h':=map δ). |

1651 |
apply f_equal2;trivial. |

1652 |
rewrite -> comp_assoc, -> str_map, <- comp_assoc with (h':=τ). |

1653 |
apply f_equal2;trivial. |

1654 |
rewrite -> prodhom_comp, -> id_l. |

1655 |
apply f_equal2;trivial. |

1656 |
rewrite -> f_cpr. |

1657 |
rewrite ->2 comp_assoc, -> map_comp. |

1658 |
rewrite -> coprodhom_comp. |

1659 |
rewrite -> cont_comp, -> id_l. |

1660 |
rewrite -> comp_assoc, -> map_unit. |

1661 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. |

1662 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

1663 |
rewrite <- H1. |

1664 |
rewrite -> cont_id. |

1665 |
rewrite -> coprodhom_id. |

1666 |
rewrite -> map_id, -> id_r. |

1667 |
trivial. |

1668 | |

1669 | |

1670 |
rewrite -> H2. |

1671 |
rewrite <- id_l with (f':=id) at 1. |

1672 |
rewrite <- prodhom_comp. |

1673 |
rewrite -> comp_assoc, <- liftingcofree_mapc. |

1674 |
rewrite <- comp_assoc, <- naturality_τv. |

1675 |
rewrite -> comp_assoc, -> H_main. |

1676 |
rewrite <- comp_assoc, -> prodhom_comp, -> id_l. |

1677 |
rewrite -> liftingcofree_mapc. |

1678 |
trivial. |

1679 | |

1680 |
Qed. |

1681 | |

1682 | |

1683 | |

1684 |
(* --- *) |

1685 | |

1686 | |

1687 | |

1688 |
Theorem proving_strength_iteration_guarded : forall x y z (f: x ~> coext T a b (y ⊕ x)), |

1689 |
guarded f -> |

1690 |
τv ∘ (id ×× f †') = (mapc dist2 ∘ τv ∘ (id (a:=z) ×× f)) †'. |

1691 | |

1692 |
Proof. |

1693 |
intros. |

1694 |
unfold guarded in H. |

1695 |
inversion H as [u' H']. |

1696 | |

1697 |
apply unfolding_guarded2. |

1698 |
unfold guarded. |

1699 |
exists (map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ ∘ (id ×× u')). |

1700 |
rewrite ->5 comp_assoc. |

1701 |
rewrite ->2 map_comp. |

1702 |
rewrite -> out_mapc. |

1703 |
rewrite -> coprodhom_comp, -> id_l, -> id_r. |

1704 |
rewrite <- comp_assoc with (g':=out), -> strength1. |

1705 |
rewrite <-2 comp_assoc with (f':=id ×× f), -> prodhom_comp. |

1706 |
rewrite -> H'. |

1707 |
rewrite <- prodhom_comp. |

1708 |
rewrite ->3 comp_assoc; apply f_equal2;trivial. |

1709 |
rewrite -> comp_assoc, ->2 map_comp. |

1710 |
rewrite -> coprodhom_comp, -> id_l. |

1711 |
rewrite -> cont_comp. |

1712 |
rewrite <- comp_assoc, <- str_map. |

1713 |
rewrite -> comp_assoc; apply f_equal2;trivial. |

1714 |
rewrite -> map_comp; apply f_equal1. |

1715 |
rewrite <- cont_id. |

1716 |
rewrite <- comp_assoc, <- delta. |

1717 |
rewrite -> prodhom_id. |

1718 |
rewrite -> cont_id. |

1719 |
rewrite -> comp_assoc with (g':=(id ×× inl ⊕⊕ id)), -> coprodhom_comp, -> id_l. |

1720 |
apply f_equal2;trivial. |

1721 |
apply f_equal2;trivial. |

1722 |
apply dist2_inl. |

1723 | |

1724 | |

1725 |
rewrite <- proving_unfolding at 1. |

1726 |
rewrite <- id_l with (f':=id) at 1. |

1727 |
rewrite <- prodhom_comp. |

1728 |
rewrite -> comp_assoc, <- proving_str4. |

1729 | |

1730 |
assert (aux: ([ηv, τv ∘ (id ×× f †')]) ∘ dist2 = τv ∘ (id (a:=z) ×× [ηv, f †'])). |

1731 |
unfold dist2. |

1732 |
rewrite -> comp_assoc, <- uncurry2. |

1733 |
rewrite -> f_cpr. |

1734 |
rewrite ->2 curry2. |

1735 |
rewrite -> comp_assoc, -> cpr_inl. |

1736 |
rewrite -> comp_assoc, -> cpr_inr. |

1737 |
apply swapp_switch. |

1738 |
apply curry_cong. |

1739 |
rewrite -> curry_uncurry. |

1740 |
case_distinction. |

1741 |
rewrite -> cpr_inl. |

1742 |
rewrite -> curry1. |

1743 |
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. |

1744 |
rewrite -> comp_assoc with (g':=id ×× inl), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp. |

1745 |
rewrite -> cpr_inl, -> id_l. |

1746 |
rewrite -> proving_str3. |

1747 |
trivial. |

1748 |
rewrite -> cpr_inr. |

1749 |
rewrite -> curry1. |

1750 |
rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. |

1751 |
rewrite -> comp_assoc with (g':=id ×× inr), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp. |

1752 |
rewrite -> cpr_inr, -> id_l. |

1753 |
trivial. |

1754 |
rewrite <- aux; clear aux. |

1755 | |

1756 | |

1757 |
rewrite <- liftingcofree_mapc. |

1758 |
rewrite ->2 comp_assoc. |

1759 |
trivial. |

1760 |
Qed. |

1761 | |

1762 | |

1763 | |

1764 |
Theorem proving_strength_iteration : forall x y (f: x ~> coext T a b (y ⊕ x)), |

1765 |
τv ∘ (id ×× f †') = ((ηv ∘ dist2) § ∘ τv ∘ (id (a:=x) ×× f)) †'. |

1766 | |

1767 |
Proof. |

1768 |
intros. |

1769 |
rewrite <- mapc_unfold. |

1770 | |

1771 | |

1772 |
rewrite -> itercofree_triangle. |

1773 | |

1774 |
rewrite -> proving_strength_iteration_guarded. |

1775 | |

1776 |
symmetry; rewrite -> itercofree_triangle; symmetry. |

1777 | |

1778 | |

1779 |
apply f_equal1. |

1780 |
unfold triangle. |

1781 | |

1782 |
rewrite <- id_l with (f':=id). |

1783 |
rewrite <- comp_assoc with (h':=tuo), <- prodhom_comp, -> id_l, -> comp_assoc. |

1784 | |

1785 | |

1786 |
assert (bottom_triangle: tuo ∘ map (dist2 ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ |

1787 |
= mapc (dist2 (x:=x) (y:=y)) ∘ τv ∘ (id (a:=x) ×× tuo (a:=a) (b:=b))). |

1788 |
symmetry. |

1789 | |

1790 |
assert (aux2: τv (x:=x) (y:=(y ⊕ x)) (a:=a) (b:=b) = tuo ∘ map (id ⊕⊕ cont τv) ∘ map δ ∘ τ ∘ (id ×× out)). |

1791 |
apply out_cong. |

1792 |
rewrite -> strength1. |

1793 |
rewrite ->4 comp_assoc with (h':=out). |

1794 |
rewrite -> out_tuo_is_id, -> id_r. |

1795 |
trivial. |

1796 |
rewrite -> aux2 at 1; clear aux2. |

1797 | |

1798 |
rewrite <-2 comp_assoc with (f':=id ×× tuo), -> prodhom_comp, -> id_r. |

1799 |
rewrite -> out_tuo_is_id, -> prodhom_id, -> id_l. |

1800 | |

1801 |
apply out_cong. |

1802 |
rewrite ->7 comp_assoc. |

1803 |
rewrite -> out_tuo_is_id, -> id_r. |

1804 |
rewrite -> out_mapc. |

1805 |
rewrite <- comp_assoc with (g':=out), -> out_tuo_is_id, -> id_l. |

1806 |
rewrite -> map_comp. |

1807 |
rewrite -> coprodhom_comp, -> id_l. |

1808 |
rewrite -> cont_comp. |

1809 |
trivial. |

1810 |
rewrite <- bottom_triangle. |

1811 | |

1812 |
assert (aux3: (id ×× map (inl ⊕⊕ id)) ∘ (id ×× ((π ∘ out) ∘ f) †) |

1813 |
= id (a:=x) ×× map (inl (b:=x) ⊕⊕ id) ∘ ((π ∘ out) ∘ f) †). |

1814 |
rewrite -> prodhom_comp. |

1815 |
rewrite -> id_l. |

1816 |
trivial. |

1817 |
rewrite <- aux3; clear aux3. |

1818 | |

1819 |
rewrite -> comp_assoc with (g':=id ×× map (inl ⊕⊕ id)). |

1820 |
rewrite <-5 comp_assoc with (h':=tuo). |

1821 |
apply f_equal2; trivial. |

1822 | |

1823 | |

1824 |
assert (middle_square: map (inl ⊕⊕ id) ∘ map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ = |

1825 |
map (dist2 ⊕⊕ cont (mapc (dist2 (x:=x) (y:=y)) ∘ τv (a:=a) (b:=b))) ∘ map (δ (a:=a) (b:=b)) ∘ τ ∘ (id (a:=x) ×× map (inl (a:=y) (b:=x) ⊕⊕ id))). |

1826 |
rewrite <- comp_assoc with (g':=τ), <- str_map. |

1827 |
rewrite <-2 comp_assoc with (g':=map δ). |

1828 |
rewrite -> comp_assoc with (h':=map δ), -> map_comp with (g:=id ×× (inl ⊕⊕ id)), <-2 cont_id. |

1829 |
rewrite <- delta. |

1830 |
rewrite -> prodhom_id. |

1831 |
rewrite ->2 cont_id. |

1832 |
rewrite ->2 comp_assoc, ->3 map_comp. |

1833 |
rewrite -> comp_assoc, ->2 coprodhom_comp, ->2 id_l, -> id_r. |

1834 |
rewrite -> dist2_inl. |

1835 |
trivial. |

1836 |
rewrite <- middle_square. |

1837 | |

1838 |
rewrite <- comp_assoc with (f':=map δ), -> map_comp. |

1839 | |

1840 |
set (p:= (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ δ). |

1841 | |

1842 |
rewrite <-2 comp_assoc with (h':=map (inl ⊕⊕ id)). |

1843 |
apply f_equal2; trivial. |

1844 | |

1845 |
(* top triangle *) |

1846 |
rewrite <- comp_assoc, -> strength_iteration. |

1847 |
rewrite -> map_naturality. |

1848 | |

1849 |
assert (aux4: (id ×× π) ∘ (id ×× out) ∘ (id ×× f) |

1850 |
= id (a:=x) ×× (π ∘ out) ∘ f). |

1851 |
rewrite ->2 prodhom_comp. |

1852 |
rewrite ->2 id_l. |

1853 |
trivial. |

1854 |
rewrite <- aux4; clear aux4. |

1855 | |

1856 |
unfold π. |

1857 |
rewrite <- comp_assoc with (g':=τ), ->2 comp_assoc with (h':=τ), <- str_map. |

1858 |
rewrite -> comp_assoc, -> map_comp. |

1859 |
rewrite ->3 comp_assoc, -> map_comp. |

1860 |
apply f_equal1. |

1861 |
rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc. |

1862 |
rewrite ->3 comp_assoc, -> map_comp. |

1863 |
apply f_equal2; trivial. |

1864 |
rewrite <- comp_assoc with (g':=out), -> strength1. |

1865 |
rewrite -> comp_assoc with (f':=id ×× out);apply f_equal2; trivial. |

1866 |
rewrite -> comp_assoc with (f':=τ); apply f_equal2; trivial. |

1867 |
rewrite ->2 map_comp. |

1868 |
apply f_equal1. |

1869 |
rewrite <- comp_assoc with (g':=dist2 ⊕⊕ cont (mapc dist2)), -> comp_assoc with (g':=id ⊕⊕ cont τv), |

1870 |
-> coprodhom_comp. |

1871 |
rewrite -> cont_comp, -> id_l. |

1872 |
rewrite -> comp_assoc, -> cpr_coprodhom. |

1873 |
unfold δ. |

1874 |
rewrite -> comp_assoc, -> cpr_coprodhom, -> id_l. |

1875 |
unfold dist2 at 4. |

1876 |
rewrite -> comp_assoc, <- uncurry2, -> f_cpr. |

1877 |
rewrite ->2 curry2. |

1878 |
rewrite -> comp_assoc, -> cpr_inl. |

1879 |
rewrite -> comp_assoc, -> cpr_inr. |

1880 |
symmetry; apply swapp_switch; symmetry. |

1881 |
apply curry_cong. |

1882 |
rewrite -> curry_uncurry. |

1883 | |

1884 |
case_distinction. |

1885 | |

1886 |
rewrite -> cpr_inl. |

1887 |
rewrite -> curry1. |

1888 |
rewrite <- comp_assoc, -> swap_prodhom. |

1889 |
rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp. |

1890 |
rewrite -> cpr_inl, -> id_l. |

1891 |
rewrite <- comp_assoc with (g':=dist2), <- naturality_dist2. |

1892 |
rewrite -> comp_assoc, -> coprodhom_comp. |

1893 |
rewrite -> prodhom_id, -> id_l. |

1894 |
apply f_equal1. |

1895 |
apply f_equal2;trivial. |

1896 |
apply f_equal2;trivial. |

1897 |
apply f_equal2;trivial. |

1898 |
unfold p. |

1899 |
unfold δ. |

1900 |
rewrite <-2 comp_assoc. |

1901 |
rewrite -> dist2_inl. |

1902 |
rewrite -> coprodhom_inl, -> id_l. |

1903 |
rewrite -> coprodhom_inl, -> id_l. |

1904 |
trivial. |

1905 | |

1906 |
rewrite -> cpr_inr. |

1907 |
rewrite -> curry1, <- comp_assoc. |

1908 |
rewrite -> swap_prodhom. |

1909 |
rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp. |

1910 |
rewrite -> cpr_inr. |

1911 |
rewrite <- prodhom_comp. |

1912 |
rewrite <- comp_assoc with (g':=dist2), -> comp_assoc with (h':=dist2), -> dist2_inl. |

1913 |
rewrite -> comp_assoc, -> coprodhom_inl. |

1914 |
apply f_equal1. |

1915 |
apply f_equal2;trivial. |

1916 |
rewrite <-3 comp_assoc; apply f_equal2;trivial. |

1917 |
unfold p. |

1918 |
unfold δ. |

1919 |
rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l. |

1920 |
rewrite <- comp_assoc, -> dist2_inr. |

1921 |
rewrite -> coprodhom_inr, -> comp_assoc. |

1922 |
trivial. |

1923 | |

1924 |
apply guardedtriangle_def. |

1925 | |

1926 |
Qed. |

1927 | |

1928 | |

1929 | |

1930 |
(* incorporate parameters a, b into definitions for the instance declaration; |

1931 |
this doesn't change the significance of the proofs established above *) |

1932 |
Definition ηv' (x : Obj) := |

1933 |
ηv (x:=x) (a:=a) (b:=b). |

1934 | |

1935 |
Definition lifting_cofree' (x y : Obj) (f: x ~> coext T a b y) := |

1936 |
f §. |

1937 | |

1938 |
Definition iter_cofree' (x y : Obj) (f: x ~> coext T a b (y ⊕ x)) := |

1939 |
f †'. |

1940 | |

1941 |
Definition τv' (x y : Obj) := |

1942 |
τv (x:=x) (y:=y) (a:=a) (b:=b). |

1943 | |

1944 | |

1945 |
(* Proof that a cofree extension is an ElgotMonad *) |

1946 |
Instance cofree : ElgotMonad Obj Hom0 C (coext T a b) := { |

1947 |
η := ηv'; |

1948 |
lifting := lifting_cofree'; |

1949 |
iter := iter_cofree'; |

1950 |
τ := τv' |

1951 |
}. |

1952 | |

1953 |
Proof. |

1954 | |

1955 |
apply proving_kl1. |

1956 | |

1957 |
apply proving_kl2. |

1958 | |

1959 |
apply proving_kl3. |

1960 | |

1961 |
apply proving_str1. |

1962 | |

1963 |
apply proving_str2. |

1964 | |

1965 |
apply proving_str3. |

1966 | |

1967 |
apply proving_str4. |

1968 | |

1969 |
apply proving_unfolding. |

1970 | |

1971 |
apply proving_naturality. |

1972 | |

1973 |
apply proving_dinaturality. |

1974 | |

1975 |
apply proving_codiagonal. |

1976 | |

1977 |
apply proving_uniformity. |

1978 | |

1979 |
apply proving_strength_iteration. |

1980 | |

1981 |
Qed. |

1982 | |

1983 |
(* |

1984 |
Print Assumptions cofree. |

1985 |
*) |

1986 | |

1987 | |

1988 |
End ContextCofreeElgotMonad. |