## corque / Lemmas_CofreeElgotMonad.v @ 4806fe22

History | View | Annotate | Download (34.7 KB)

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

2 |
Require Import biCCC. |

3 |
Require Import Lemmas_biCCC. |

4 |
Require Import Coq_Steroids. |

5 |
Require Import ElgotMonad. |

6 |
Require Import Lemmas_ElgotMonad. |

7 |
Require Import CofreeElgotMonad. |

8 |
Require Import Setoid. |

9 |
Open Scope c_scope. |

10 |
Section Lemmas. |

11 |
Context `(CofreeElgotMonad). |

12 | |

13 |
(* Lemmas proven in the following: |

14 | |

15 | |

16 |
cont_id : |

17 |
cont id = id |

18 | |

19 |
cont_comp : |

20 |
cont f ∘ cont g = cont (f ∘ g) |

21 | |

22 |
fusion: |

23 |
u ∘ v = map (id ⊕⊕ cont v) ∘ w -> |

24 |
coit w = (coit u) ∘ v. |

25 | |

26 |
coit_of_out_is_id: |

27 |
coit (out) = id |

28 | |

29 |
tuo_out_is_id: |

30 |
tuo ∘ out = id |

31 | |

32 |
out_tuo_is_id: |

33 |
out ∘ tuo = id |

34 | |

35 |
out_cong: |

36 |
out ∘ f = out ∘ g -> f = g |

37 | |

38 |
out_mapc: |

39 |
out ∘ mapc f = |

40 |
map (f ⊕⊕ cont (mapc f)) ∘ out |

41 | |

42 |
out_unitcofree: |

43 |
out ∘ ηv = η ∘ inl |

44 | |

45 |
mapc_id: |

46 |
mapc (a:=a) (b:=b) (id (a:=x)) = id |

47 | |

48 |
mapc_comp: |

49 |
mapc f ∘ mapc g = mapc (f ∘ g) |

50 | |

51 |
mapc_unitcofree |

52 |
mapc u ∘ ηv = ηv ∘ u |

53 | |

54 |
mapc_coit (fusion!) |

55 |
mapc s ∘ coit t = coit (map (s ⊕⊕ id) ∘ t) |

56 | |

57 |
mapc_liftingcofree (fusion!) |

58 |
mapc s ∘ t § = coit (([map(s ⊕⊕ cont (mapc inr)) ∘ out ∘ [t, ηv], |

59 |
η ∘ inr]) * ∘ out) ∘ mapc inl |

60 | |

61 |
mapc_liftingcofree_unfolded (fusion!) |

62 |
mapc s ∘ (coit |

63 |
(([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ [t, ηv], |

64 |
η ∘ inr]) * ∘ out) ∘ mapc inl) = coit (([map(s ⊕⊕ id ×× mapc inr ^^ id) ∘ out ∘ [t, ηv], |

65 |
η ∘ inr]) * ∘ out) ∘ mapc inl |

66 | |

67 |
liftingcofree_unfoldtocpr: |

68 |
f § = [f, ηv] § ∘ mapc inl |

69 | |

70 |
liftingdef_with_inr: |

71 |
coit (([(map (id ⊕⊕ cont (mapc inr)) ∘ out) |

72 |
∘ [t, ηv], η ∘ inr]) * ∘ out) ∘ mapc inr = id |

73 | |

74 |
lifting1: |

75 |
out ∘ t § = [out ∘ t, η ∘ inr ∘ cont (t §)]* ∘ out |

76 | |

77 |
lifting2: |

78 |
out ∘ s = [out ∘ t, η ∘ inr ∘ cont s]* ∘ out -> |

79 |
s = t § |

80 | |

81 |
guardedtriangle: |

82 |
guarded f -> ▷ f = f |

83 | |

84 |
guardedtriangle_def: |

85 |
guarded (▷ f) |

86 | |

87 |
itercofree_triangle: |

88 |
f †' = (▷ f) †' |

89 | |

90 |
liftingcofree_tuo: |

91 |
[ηv, t] § ∘ tuo = tuo ∘ [[η ∘ inl, out ∘ t], η ∘ inr ∘ cont ([ηv, t] §)] * |

92 | |

93 |
unfolding_guarded1: |

94 |
guarded f -> f †' = [ηv, f †'] § ∘ f |

95 | |

96 |
unfolding_guarded2: |

97 |
guarded f -> g = [ηv, g] § ∘ f -> g = f †' |

98 | |

99 |
unfolding_triangle1: |

100 |
f †' = [ηv, f †'] § ∘ ▷ f |

101 | |

102 |
unfolding_triangle2: |

103 |
g = [ηv, g] § ∘ ▷ f -> g = f †' |

104 | |

105 |
out_itercofree: |

106 |
out ∘ f †' = ([η ∘ inl, (η ∘ inr) ∘ cont ([ηv, f †'] §)) * |

107 |
∘ ((π ∘ out) ∘ f) † |

108 | |

109 |
strength1: |

110 |
out ∘ τv = map (id ⊕⊕ cont τv) ∘ map δ ∘ τ ∘ (id ×× out) |

111 | |

112 |
strength2: |

113 |
out ∘ f = map (id ⊕⊕ cont f) ∘ map δ ∘ τ ∘ (id ×× out) -> |

114 |
f = τv |

115 | |

116 |
out_itercofree2: |

117 |
out ∘ f †' = (map ([[inl ∘ inl, inr], inl ∘ inr ∘ cont ([ηv, f †'] §)]) ∘ out ∘ f) † |

118 | |

119 |
out_triangle: |

120 |
out ∘ ▷ f = (map ([[inl ∘ inl ∘ inl, inr], inl ∘ inr]) ∘ out ∘ f) † |

121 | |

122 |
out_triangle2: |

123 |
out ∘ mapc (c_assoc2 ∘ (id ⊕⊕ swapc) ∘ c_assoc1) ∘ ▷ (mapc (c_assoc2 ∘ (id ⊕⊕ swapc) ∘ c_assoc1) ∘ g) |

124 |
= (map ([[[inl ∘ inl ∘ inl ∘ inl, inr], inl ∘ inl ∘ inr], inl ∘ inr]) ∘ out ∘ g) † |

125 | |

126 |
delta: |

127 |
(f ×× g ⊕⊕ cont (f ×× h)) ∘ δ = δ ∘ (f ×× (g ⊕⊕ cont h)) |

128 | |

129 |
naturality_τv: ADMITTED |

130 |
τv ∘ (f ×× mapc g) = mapc (f ×× g) ∘ τv |

131 | |

132 |
p_assoc_delta : |

133 |
(p_assoc1 ⊕⊕ cont p_assoc1) ∘ δ = δ ∘ ((id ×× δ) ∘ p_assoc1) |

134 | |

135 |
*) |

136 | |

137 | |

138 |
Lemma cont_id : forall |

139 |
(x a b : Obj), |

140 |
cont (a:=a) (b:=b) (id (a:=x)) = id. |

141 | |

142 |
Proof. |

143 |
intros. |

144 |
unfold cont. |

145 |
rewrite -> post_comp_id, -> prodhom_id. |

146 |
trivial. |

147 |
Qed. |

148 | |

149 | |

150 | |

151 |
Lemma cont_comp : forall |

152 |
(x y z a b : Obj) |

153 |
(f: y ~> z ) |

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

155 |
cont f ∘ cont g = cont (a:=a) (b:=b) (f ∘ g). |

156 | |

157 |
Proof. |

158 |
intros. |

159 |
unfold cont. |

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

161 |
rewrite -> post_comp_comp. |

162 |
trivial. |

163 |
Qed. |

164 | |

165 | |

166 | |

167 |
Lemma fusion : forall |

168 |
(A B a b x : Obj) |

169 |
(u: B ~> T (x ⊕ a × (exp B b))) |

170 |
(v: A ~> B) |

171 |
(w: A ~> T (x ⊕ a × (exp A b))), |

172 |
u ∘ v = map (id ⊕⊕ cont v) ∘ w -> |

173 |
coit w = (coit u) ∘ v. |

174 | |

175 |
Proof. |

176 |
intros. |

177 |
symmetry. |

178 |
apply coit2. |

179 |
rewrite -> comp_assoc with (h':= out), -> coit1. |

180 |
rewrite <- comp_assoc with (f':=v), -> H0. |

181 |
rewrite -> comp_assoc with (f':=w), -> map_comp. |

182 |
apply f_equal2; trivial. |

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

184 |
trivial. |

185 |
Qed. |

186 | |

187 | |

188 | |

189 |
Lemma coit_of_out_is_id : forall |

190 |
(A x a b : Obj), |

191 |
coit (out (x:=x) (a:=a) (b:=b)) = id. |

192 | |

193 |
Proof. |

194 |
intros. |

195 |
symmetry. |

196 |
apply coit2. |

197 |
rewrite -> id_l, -> cont_id, -> coprodhom_id. |

198 |
rewrite -> map_id, -> id_r; trivial. |

199 |
Qed. |

200 | |

201 | |

202 | |

203 |
Lemma tuo_out_is_id : forall |

204 |
(x a b : Obj), |

205 |
tuo (x:=x) (a:=a) (b:=b) ∘ out = id. |

206 | |

207 |
Proof. |

208 |
intros. |

209 |
unfold tuo. |

210 |
rewrite <- fusion with (w:=out). |

211 |
rewrite -> coit_of_out_is_id. |

212 |
trivial. trivial. trivial. |

213 |
Qed. |

214 | |

215 | |

216 | |

217 |
Lemma out_tuo_is_id : forall |

218 |
(x a b : Obj), |

219 |
out (x:=x) (a:=a) (b:=b) ∘ tuo = id. |

220 | |

221 |
Proof. |

222 |
intros. |

223 |
unfold tuo. |

224 |
rewrite -> coit1. |

225 |
rewrite -> map_comp. |

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

227 |
rewrite -> tuo_out_is_id. |

228 |
rewrite -> cont_id, -> coprodhom_id, -> map_id. |

229 |
trivial. |

230 |
Qed. |

231 | |

232 | |

233 | |

234 |
Lemma out_cong : forall |

235 |
(x y a b : Obj) |

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

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

238 |
out ∘ f = out ∘ g -> f = g. |

239 | |

240 |
Proof. |

241 |
intros. |

242 |
transitivity (tuo ∘ out ∘ f). |

243 |
rewrite -> tuo_out_is_id. |

244 |
rewrite -> id_r; trivial. |

245 |
transitivity (tuo ∘ out ∘ g). |

246 |
rewrite <- comp_assoc, -> H0. |

247 |
rewrite <- comp_assoc; trivial. |

248 |
rewrite -> tuo_out_is_id, -> id_r; trivial. |

249 |
Qed. |

250 | |

251 | |

252 | |

253 |
Lemma tuo_cong : forall |

254 |
(x y a b : Obj) |

255 |
(f: x ~> T (y ⊕ a × ((coext T a b y) ^ b))) |

256 |
(g: x ~> T (y ⊕ a × ((coext T a b y) ^ b))), |

257 |
tuo ∘ f = tuo ∘ g -> f = g. |

258 | |

259 |
Proof. |

260 |
intros. |

261 |
assert (out ∘ tuo ∘ f = out ∘ tuo ∘ g). |

262 |
rewrite <-2 comp_assoc. |

263 |
congruence. |

264 |
rewrite -> out_tuo_is_id in H1. |

265 |
rewrite ->2 id_r in H1; trivial. |

266 |
Qed. |

267 | |

268 | |

269 | |

270 |
Lemma out_mapc : forall |

271 |
(x y a b : Obj) |

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

273 |
out ∘ mapc f = |

274 |
map (f ⊕⊕ cont (mapc f)) ∘ out (a:=a) (b:=b). |

275 | |

276 |
Proof. |

277 |
intros. |

278 |
unfold mapc. |

279 |
rewrite -> coit1. |

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

281 |
rewrite -> map_comp. |

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

283 |
trivial. |

284 |
Qed. |

285 | |

286 | |

287 | |

288 |
Lemma out_unitcofree : forall |

289 |
(x a b : Obj), |

290 |
out (a:=a) (b:=b) ∘ ηv = η ∘ inl (a:=x). |

291 | |

292 |
Proof. |

293 |
intros. |

294 |
unfold ηv. |

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

296 |
trivial. |

297 |
Qed. |

298 | |

299 | |

300 | |

301 |
Lemma mapc_id : forall |

302 |
(x a b : Obj), |

303 |
mapc (a:=a) (b:=b) (id (a:=x)) = id. |

304 | |

305 |
Proof. |

306 |
intros. |

307 |
unfold mapc. |

308 |
rewrite -> coprodhom_id. |

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

310 |
apply coit_of_out_is_id; trivial. |

311 |
Qed. |

312 | |

313 | |

314 | |

315 |
Lemma mapc_comp : forall |

316 |
(x y z a b : Obj) |

317 |
(f: y ~> z) |

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

319 |
mapc f ∘ mapc g = mapc (a:=a) (b:=b) (f ∘ g). |

320 | |

321 |
Proof. |

322 |
intros. |

323 |
unfold mapc. |

324 |
apply coit2. |

325 |
rewrite -> comp_assoc with (h':=out), -> coit1. |

326 |
rewrite -> comp_assoc with (f':=out), -> map_comp. |

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

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

329 |
rewrite ->2 coprodhom_comp, ->2 id_l, -> cont_comp, -> id_r. |

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

331 |
trivial. |

332 |
Qed. |

333 | |

334 | |

335 | |

336 |
Lemma mapc_unitcofree : forall |

337 |
(x y a b : Obj) (f: x ~> y), |

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

339 | |

340 |
Proof. |

341 |
intros. |

342 |
unfold mapc. |

343 |
apply out_cong. |

344 |
rewrite -> comp_assoc, -> coit1. |

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

346 |
rewrite -> comp_assoc with (f':=out), -> map_comp. |

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

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

349 |
rewrite -> comp_assoc with (f':=inl), -> map_unit. |

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

351 |
rewrite -> comp_assoc; trivial. |

352 |
Qed. |

353 | |

354 | |

355 | |

356 |
Lemma mapc_coit : forall |

357 |
(x y z a b : Obj) |

358 |
(f: y ~> z) |

359 |
(g: x ~> T (y ⊕ a × (x ^ b))), |

360 |
mapc f ∘ coit g = coit (map (f ⊕⊕ id) ∘ g). |

361 | |

362 |
Proof. |

363 |
intros. |

364 |
unfold mapc. |

365 |
rewrite <- fusion with (w:= map (f ⊕⊕ id) ∘ g). |

366 |
trivial. |

367 |
rewrite <- comp_assoc, -> coit1. |

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

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

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

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

372 |
trivial. |

373 |
Qed. |

374 | |

375 | |

376 | |

377 |
Lemma liftingcofree_unfoldtocpr : forall |

378 |
(x y a b : Obj) |

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

380 |
f § = [f, ηv] § ∘ mapc inl. |

381 | |

382 |
Proof. |

383 |
intros. |

384 |
unfold lifting_cofree. |

385 |
apply f_equal2; trivial. |

386 |
symmetry. |

387 |
apply coit2. |

388 |
rewrite -> comp_assoc, -> coit1. |

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

390 |
rewrite <- comp_assoc with (f':=mapc inl), -> out_mapc. |

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

392 |
rewrite <- comp_assoc with (f':=inl ⊕⊕ cont (mapc inl)), -> cpr_coprodhom. |

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

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

395 | |

396 |
rewrite -> map_lifting. |

397 |
rewrite -> f_cpr. |

398 |
rewrite -> f_cpr with (h:=η ∘ inr). |

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

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

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

402 |
rewrite ->2 coprodhom_inr. |

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

404 |
apply f_equal1; apply f_equal2; trivial. |

405 | |

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

407 |
apply f_equal2; trivial; |

408 |
apply f_equal2; trivial. |

409 |
apply f_equal1. |

410 |
rewrite ->2 coprodhom_comp, -> id_l, ->2 cont_comp. |

411 |
apply f_equal2; trivial. |

412 |
apply f_equal1. |

413 |
rewrite <-2 comp_assoc, -> mapc_comp. |

414 | |

415 | |

416 |
transitivity (coit (out (a:=a) (b:=b)(x:=y))). |

417 | |

418 |
symmetry. |

419 |
apply fusion. |

420 | |

421 |
rewrite <- comp_assoc, -> out_mapc. |

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

423 |
rewrite -> lifting_map. |

424 |
rewrite -> cpr_coprodhom. |

425 |
rewrite <-2 comp_assoc, -> cpr_inr. |

426 |
rewrite -> out_unitcofree. |

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

428 |
rewrite <- comp_assoc, -> coprodhom_inl, -> id_l. |

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

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

431 |
trivial. |

432 | |

433 | |

434 |
apply fusion. |

435 | |

436 |
rewrite <- comp_assoc, -> out_mapc. |

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

438 |
rewrite -> lifting_map. |

439 |
rewrite -> cpr_coprodhom. |

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

441 |
rewrite -> cpr_inr. |

442 |
rewrite -> out_unitcofree. |

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

444 |
rewrite <- comp_assoc, -> coprodhom_inl, -> id_l. |

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

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

447 |
trivial. |

448 | |

449 |
Qed. |

450 | |

451 | |

452 | |

453 |
Lemma liftingdef_with_inr : forall |

454 |
(x y a b : Obj) |

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

456 |
coit (([(map (id ⊕⊕ cont (mapc inr)) ∘ out) |

457 |
∘ [f, ηv], η ∘ inr]) * ∘ out) ∘ mapc inr = id. |

458 | |

459 |
Proof. |

460 |
intros. |

461 |
rewrite <- coit_of_out_is_id; trivial. |

462 |
symmetry. |

463 |
apply fusion. |

464 |
rewrite <- comp_assoc, -> out_mapc. |

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

466 |
rewrite -> cpr_coprodhom. |

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

468 |
rewrite <- comp_assoc with (f':=ηv), -> out_unitcofree. |

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

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

471 |
rewrite <- comp_assoc with (g':=inr), <- f_cpr. |

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

473 |
trivial. |

474 |
Qed. |

475 | |

476 | |

477 | |

478 |
Lemma lifting1 : forall |

479 |
(x y a b : Obj) |

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

481 |
out ∘ f § = [out ∘ f, η ∘ inr ∘ cont (f §)]* ∘ out. |

482 | |

483 |
Proof. |

484 |
intros. |

485 |
unfold lifting_cofree. |

486 |
rewrite -> comp_assoc, -> coit1. |

487 | |

488 |
rewrite <- comp_assoc, <- comp_assoc with (f':=mapc inl), -> out_mapc. |

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

490 |
rewrite <- comp_assoc, -> lifting_map. |

491 |
rewrite -> cpr_coprodhom. |

492 |
rewrite -> map_lifting. |

493 |
apply f_equal1. |

494 | |

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

496 |
rewrite -> f_cpr. |

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

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

499 | |

500 |
rewrite -> liftingdef_with_inr. |

501 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

502 | |

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

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

505 |
rewrite -> comp_assoc with (g':=inr), <- comp_assoc with (f':=cont (mapc inl)); |

506 |
rewrite -> cont_comp. |

507 |
trivial. |

508 |
Qed. |

509 | |

510 | |

511 | |

512 |
Lemma lifting2 : forall |

513 |
(x y a b : Obj) |

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

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

516 |
out ∘ g = [out ∘ f, η ∘ inr ∘ cont g]* ∘ out -> |

517 |
g = f §. |

518 | |

519 |
Proof. |

520 |
intros. |

521 | |

522 |
(* The idea is to introduce such w: T_a^b x + T_a^b y -> T_a^b y |

523 |
that w inl = g and w inr = id *) |

524 | |

525 |
remember (coit ([[(map (id ⊕⊕ cont inr)) ∘ out ∘ f, |

526 |
η ∘ inr ∘ cont inl]* ∘ out, |

527 |
(map (id ⊕⊕ cont inr)) ∘ out])) as w eqn:W. |

528 | |

529 |
assert ([g, id] = [f§, id]). |

530 |
transitivity w. |

531 | |

532 |
rewrite -> W. |

533 |
apply coit2. |

534 |
rewrite ->2 f_cpr, -> id_l. |

535 | |

536 |
case_distinction. |

537 | |

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

539 |
rewrite -> f_cpr. |

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

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

542 |
rewrite -> cpr_inr, -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

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

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

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

546 |
rewrite -> cpr_inl. |

547 |
exact H0. |

548 | |

549 |
rewrite -> comp_assoc, -> map_comp, -> coprodhom_comp, -> id_l, -> cont_comp. |

550 |
rewrite -> cpr_inr. |

551 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

552 |
trivial. |

553 | |

554 | |

555 |
rewrite -> W. |

556 |
symmetry. |

557 |
apply coit2. |

558 | |

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

560 |
rewrite -> f_cpr. |

561 | |

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

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

564 |
rewrite -> cpr_inr. |

565 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

566 |
apply f_equal2;trivial. |

567 | |

568 |
rewrite -> map_lifting. |

569 |
rewrite -> f_cpr. |

570 |
rewrite -> comp_assoc with (f':=f), -> comp_assoc, -> map_comp. |

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

572 |
rewrite -> cpr_inr. |

573 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

574 | |

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

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

577 |
rewrite <-2 comp_assoc with (f':=cont inl), -> cont_comp. |

578 |
rewrite -> cpr_inl. |

579 |
rewrite -> comp_assoc; apply lifting1. |

580 |
trivial. |

581 | |

582 |
apply f_equal1 with (f:= fun x => x ∘ inl) in H1. |

583 |
rewrite ->2 cpr_inl in H1; trivial. |

584 | |

585 |
Qed. |

586 | |

587 | |

588 | |

589 |
Lemma guardedtriangle : forall |

590 |
(x y z a b : Obj) |

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

592 |
guarded f' -> ▷ f' = f'. |

593 | |

594 |
Proof. |

595 |
intros. |

596 |
unfold guarded in H0; inversion H0 as [u' H1]. |

597 | |

598 |
apply out_cong. |

599 | |

600 |
unfold triangle. |

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

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

603 |
apply f_equal1. |

604 |
unfold π. |

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

606 |
rewrite -> cpr_coprodhom. |

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

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

609 |
rewrite -> mapinl_f_iter. |

610 |
trivial. |

611 |
Qed. |

612 | |

613 | |

614 | |

615 |
(* ▷ f is guarded by definition *) |

616 |
Lemma guardedtriangle_def : forall |

617 |
(x y a b : Obj) |

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

619 |
guarded (▷ f). |

620 | |

621 |
Proof. |

622 |
intros. |

623 |
unfold guarded, triangle. |

624 |
rewrite ->2 comp_assoc. |

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

626 |
rewrite <- comp_assoc with (g':=out); |

627 |
exists ((π ∘ (out ∘ f)) †). |

628 |
trivial. |

629 |
Qed. |

630 | |

631 | |

632 | |

633 |
Lemma itercofree_triangle : forall |

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

635 |
f †' = (▷ f) †'. |

636 | |

637 |
Proof. |

638 |
intros. |

639 |
unfold triangle, iter_cofree. |

640 | |

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

642 |
rewrite -> out_tuo_is_id, -> id_l. |

643 |
unfold π at 2. |

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

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

646 |
rewrite -> coprodhom_inl. |

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

648 |
rewrite -> mapinl_f_iter. |

649 |
trivial. |

650 |
Qed. |

651 | |

652 | |

653 | |

654 |
Lemma liftingcofree_tuo : forall |

655 |
(x y a b : Obj) |

656 |
(t: x ~> coext T a b y), |

657 |
[ηv, t] § ∘ tuo = tuo ∘ [[η ∘ inl, out ∘ t], η ∘ inr ∘ cont ([ηv, t] §)] *. |

658 | |

659 |
Proof. |

660 |
intros. |

661 |
unfold lifting_cofree. |

662 |
apply out_cong. |

663 |
rewrite ->2 comp_assoc, -> coit1. |

664 | |

665 |
rewrite <-2 comp_assoc with (f':=mapc inl), -> out_mapc. |

666 |
rewrite <-3 comp_assoc with (f':=tuo), -> out_tuo_is_id, -> id_l. |

667 |
rewrite <- comp_assoc, -> lifting_map. |

668 |
rewrite -> cpr_coprodhom. |

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

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

671 |
rewrite -> map_lifting; apply f_equal1. |

672 |
rewrite -> f_cpr. |

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

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

675 |
rewrite -> comp_assoc with (f':=[[ηv, t], ηv]), -> liftingdef_with_inr. |

676 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

677 |
rewrite -> f_cpr. |

678 |
rewrite -> out_unitcofree. |

679 |
apply f_equal1. |

680 | |

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

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

683 |
rewrite -> comp_assoc with (g':=inr), <- comp_assoc with (h':=η ∘ inr); |

684 |
rewrite -> cont_comp. |

685 |
trivial. |

686 |
Qed. |

687 | |

688 | |

689 | |

690 |
Lemma unfolding_guarded1 : forall |

691 |
(x y a b : Obj) |

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

693 |
guarded f -> f †' = [ηv, f †'] § ∘ f. |

694 | |

695 |
Proof. |

696 |
intros. |

697 |
unfold guarded in H0; inversion H0 as [u' H1]. |

698 | |

699 |
(* Some preparation *) |

700 | |

701 |
remember (coit (([[η ∘ inl, u'], η ∘ inr]) * ∘ out)) as w eqn:W. |

702 | |

703 |
assert (H2: f †' = w ∘ ηv ∘ inr). |

704 | |

705 |
unfold iter_cofree. |

706 |
rewrite <-2 comp_assoc with (f':=inr); |

707 |
apply f_equal1 with (f:= fun x => x ∘ (ηv ∘ inr)). |

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

709 |
unfold π. |

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

711 |
rewrite -> cpr_coprodhom. |

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

713 |
rewrite <- f_cpr. |

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

715 |
rewrite -> mapinl_f_iter. |

716 |
rewrite -> W; trivial. |

717 | |

718 |
assert (H3: ηv = (w ∘ ηv) ∘ inl). |

719 | |

720 |
rewrite -> W. |

721 |
apply out_cong. |

722 |
rewrite -> out_unitcofree. |

723 |
rewrite ->2 comp_assoc, -> coit1. |

724 |
rewrite -> comp_assoc with (f':=out), -> map_lifting. |

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

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

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

728 |
rewrite -> comp_assoc with (f':=inl), -> map_unit. |

729 |
rewrite <- comp_assoc, -> coprodhom_inl, -> id_l; trivial. |

730 | |

731 | |

732 |
(* Main part *) |

733 | |

734 |
unfold iter_cofree at 1. |

735 | |

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

737 |
unfold π. |

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

739 |
rewrite -> cpr_coprodhom. |

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

741 |
rewrite <- f_cpr. |

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

743 |
rewrite -> mapinl_f_iter. |

744 | |

745 |
apply out_cong. |

746 |
rewrite ->2 comp_assoc, -> coit1. |

747 |
rewrite -> comp_assoc with (f':=f), -> lifting1. |

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

749 |
rewrite -> out_unitcofree. |

750 |
rewrite -> comp_assoc with (f':=inl), <- comp_assoc with (f':=η), -> kl2. |

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

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

753 | |

754 |
rewrite -> H1. |

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

756 |
unfold map at 1. |

757 | |

758 |
apply f_equal2; trivial. |

759 |
apply f_equal1. |

760 |
unfold coprodhom. |

761 |
rewrite ->2 f_cpr. |

762 | |

763 |
case_distinction. |

764 |
rewrite -> id_l. |

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

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

767 |
rewrite -> out_unitcofree; trivial. |

768 | |

769 |
rewrite -> id_l. |

770 |
rewrite -> cpr_inr. |

771 |
rewrite <- comp_assoc with (g':=inr); |

772 |
apply f_equal1 with (f:= fun x => η ∘ (inr ∘ cont x)). |

773 |
rewrite <- W. |

774 |
rewrite -> H2. |

775 |
rewrite -> H3. |

776 |
rewrite <- f_cpr. |

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

778 | |

779 |
(* Curious fact: w = (w ∘ ηv) §. May be needed in the future. *) |

780 | |

781 |
apply lifting2. |

782 |
rewrite -> W at 1. |

783 | |

784 |
rewrite coit1. |

785 |
rewrite <- W. |

786 | |

787 |
rewrite -> comp_assoc with (f':=out), -> map_lifting. |

788 |
unfold map at 1. |

789 |
apply f_equal2; trivial. |

790 |
apply f_equal1. |

791 |
rewrite -> f_cpr. |

792 | |

793 |
case_distinction. |

794 |
rewrite -> W at 2. |

795 |
rewrite -> comp_assoc with (h':=out), -> coit1. |

796 |
rewrite <- W. |

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

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

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

800 |
unfold map; trivial. |

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

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

803 |
rewrite <- comp_assoc; trivial. |

804 |
Qed. |

805 | |

806 | |

807 | |

808 |
Lemma unfolding_guarded2 : forall |

809 |
(x y a b : Obj) |

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

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

812 |
guarded f -> |

813 |
g = [ηv, g] § ∘ f -> |

814 |
g = f †'. |

815 | |

816 |
Proof. |

817 |
intros. |

818 | |

819 |
rewrite -> H1. |

820 |
rewrite <- guardedtriangle with (f':=f) at 1;trivial. |

821 |
unfold triangle. |

822 |
rewrite ->2 comp_assoc, -> liftingcofree_tuo. |

823 |
unfold iter_cofree. |

824 | |

825 |
apply out_cong. |

826 |
rewrite ->3 comp_assoc, -> out_tuo_is_id, -> id_r. |

827 |
rewrite -> lifting_map. |

828 |
rewrite -> cpr_coprodhom. |

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

830 | |

831 |
rewrite ->2 comp_assoc, -> coit1. |

832 |
rewrite <-2 comp_assoc with (f':=ηv), -> out_unitcofree. |

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

834 |
rewrite -> cpr_inl. |

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

836 |
apply f_equal2;trivial. |

837 |
unfold map at 1. |

838 |
apply f_equal1. |

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

840 |
apply f_equal2;trivial. |

841 |
unfold coprodhom at 1; rewrite -> id_l. |

842 |
apply f_equal2;trivial; apply f_equal2;trivial. |

843 |
apply f_equal1. |

844 | |

845 | |

846 |
apply coit2. |

847 |
unfold lifting_cofree. |

848 |
rewrite -> comp_assoc, -> coit1. |

849 |
rewrite <-3 comp_assoc, -> out_mapc. |

850 |
rewrite ->4 comp_assoc; apply f_equal2;trivial. |

851 |
rewrite ->2 map_lifting. |

852 |
rewrite -> lifting_map. |

853 |
apply f_equal1. |

854 |
rewrite <- comp_assoc, -> cpr_coprodhom. |

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

856 | |

857 | |

858 |
case_distinction. |

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

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

861 |
rewrite -> liftingdef_with_inr. |

862 |
rewrite -> cont_id, -> coprodhom_id, -> map_id, -> id_r. |

863 | |

864 |
case_distinction. |

865 |
rewrite -> out_unitcofree. |

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

867 |
rewrite <- comp_assoc, -> coprodhom_inl, -> id_l. |

868 |
trivial. |

869 | |

870 |
rewrite -> H1 at 1. |

871 |
rewrite <- guardedtriangle with (f':=f) at 1;trivial. |

872 |
unfold triangle. |

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

874 |
rewrite -> liftingcofree_tuo. |

875 |
rewrite ->3 comp_assoc, -> out_tuo_is_id, -> id_r. |

876 |
rewrite -> lifting_map. |

877 |
rewrite -> cpr_coprodhom. |

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

879 |
apply f_equal2;trivial. |

880 |
unfold map at 1. |

881 |
apply f_equal1. |

882 | |

883 |
case_distinction. |

884 |
rewrite -> cpr_inl. |

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

886 |
rewrite -> cpr_inr. |

887 |
rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> comp_assoc with (h':=η); |

888 |
trivial. |

889 |
(* solved, because right side was equal, but the lifting unfolded *) |

890 | |

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

892 |
rewrite <-2 comp_assoc with (h':=η), -> comp_assoc with (g':=inr), ->2 coprodhom_inr. |

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

894 |
trivial. |

895 |
Qed. |

896 | |

897 | |

898 | |

899 |
Lemma unfolding_triangle1 : forall |

900 |
(x y a b : Obj) |

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

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

903 | |

904 |
Proof. |

905 |
intros. |

906 |
pose proof guardedtriangle_def (_) (_) (_) (_) (f). |

907 |
pose proof unfolding_guarded1 (_) (_) (_) (_) (▷f). |

908 |
rewrite <- itercofree_triangle in H1. |

909 |
apply H1. |

910 |
apply H0. |

911 |
Qed. |

912 | |

913 | |

914 | |

915 |
Lemma unfolding_triangle2 : forall |

916 |
(x y a b : Obj) |

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

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

919 |
g = [ηv, g] § ∘ ▷ f -> |

920 |
g = f †'. |

921 | |

922 |
Proof. |

923 |
intros. |

924 |
rewrite -> itercofree_triangle. |

925 |
apply unfolding_guarded2. |

926 |
apply guardedtriangle_def. |

927 |
apply H0. |

928 |
Qed. |

929 | |

930 | |

931 | |

932 |
Lemma out_itercofree : forall |

933 |
(x y a b : Obj) |

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

935 |
out ∘ f †' = ([η ∘ inl, η ∘ inr ∘ cont ([ηv, f †'] §)]) * |

936 |
∘ ((π ∘ out) ∘ f) †. |

937 | |

938 |
Proof. |

939 |
intros. |

940 |
rewrite -> unfolding_triangle1 at 1. |

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

942 |
unfold triangle. |

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

944 |
rewrite -> out_tuo_is_id, -> id_l. |

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

946 |
rewrite -> cpr_coprodhom. |

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

948 |
rewrite -> out_unitcofree, -> id_l. |

949 |
trivial. |

950 |
Qed. |

951 | |

952 | |

953 | |

954 |
Lemma strength1 : forall |

955 |
(x y a b : Obj), |

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

957 | |

958 |
Proof. |

959 |
intros. |

960 |
unfold τv. |

961 |
rewrite -> coit1. |

962 |
rewrite ->2 comp_assoc; trivial. |

963 |
Qed. |

964 | |

965 | |

966 | |

967 |
Lemma strength2 : forall |

968 |
(x y a b : Obj) |

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

970 |
out ∘ f = map (id ⊕⊕ cont f) ∘ map δ ∘ τ ∘ (id ×× out) -> |

971 |
f = τv. |

972 | |

973 |
Proof. |

974 |
intros. |

975 |
unfold τv. |

976 |
apply coit2. |

977 |
rewrite ->2 comp_assoc; apply H0. |

978 |
Qed. |

979 | |

980 | |

981 | |

982 |
Lemma out_itercofree2 : forall |

983 |
(x y a b : Obj) |

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

985 |
out ∘ f †' = (map ([[inl ∘ inl, inr], inl ∘ inr ∘ cont ([ηv, f †'] §)]) ∘ out ∘ f) †. |

986 | |

987 |
Proof. |

988 |
intros. |

989 |
rewrite -> out_itercofree. |

990 |
rewrite -> naturality. |

991 |
apply f_equal1. |

992 |
rewrite ->2 comp_assoc; apply f_equal2; trivial; |

993 |
apply f_equal2; trivial. |

994 |
unfold π. |

995 |
rewrite -> lifting_map. |

996 |
rewrite -> f_cpr. |

997 |
rewrite -> cpr_coprodhom. |

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

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

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

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

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

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

1004 |
unfold map. |

1005 |
rewrite -> comp_assoc; trivial. |

1006 |
Qed. |

1007 | |

1008 | |

1009 | |

1010 |
Lemma out_triangle : forall |

1011 |
(x y a b : Obj) |

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

1013 |
out ∘ ▷ f = (map ([[inl ∘ inl ∘ inl, inr], inl ∘ inr]) ∘ out ∘ f) †. |

1014 | |

1015 |
Proof. |

1016 |
intros. |

1017 |
unfold triangle. |

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

1019 |
rewrite -> map_naturality. |

1020 |
unfold π. |

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

1022 |
rewrite -> f_cpr. |

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

1024 |
rewrite -> coprodhom_inl. |

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

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

1027 |
unfold coprodhom; rewrite -> id_l. |

1028 |
rewrite -> comp_assoc; trivial. |

1029 |
Qed. |

1030 | |

1031 | |

1032 | |

1033 |
Lemma out_triangle2 : forall |

1034 |
(x y a b : Obj) |

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

1036 |
out ∘ mapc (c_assoc2 ∘ (id ⊕⊕ swapc) ∘ c_assoc1) ∘ ▷ (mapc (c_assoc2 ∘ (id ⊕⊕ swapc) ∘ c_assoc1) ∘ g) |

1037 |
= (map ([[[inl ∘ inl ∘ inl ∘ inl, inr], inl ∘ inl ∘ inr], inl ∘ inr]) ∘ out ∘ g) †. |

1038 | |

1039 |
Proof. |

1040 |
intros. |

1041 |
rewrite -> out_mapc. |

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

1043 |
rewrite -> map_naturality. |

1044 |
apply f_equal1. |

1045 |
rewrite ->2 comp_assoc with (f':=g); apply f_equal2; trivial. |

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

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

1048 |
rewrite ->2 map_comp. |

1049 |
apply f_equal1. |

1050 |
unfold c_assoc1, c_assoc2. |

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

1052 |
rewrite -> f_cpr. |

1053 |
rewrite -> cpr_coprodhom. |

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

1055 |
unfold swapc. |

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

1057 |
rewrite -> coprodhom_inr. |

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

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

1060 |
rewrite -> cpr_coprodhom. |

1061 |
rewrite -> f_cpr. |

1062 |
rewrite <-2 comp_assoc with (h':=inl), ->2 comp_assoc with (g':=inl), -> coprodhom_inl. |

1063 |
rewrite <-2 comp_assoc with (h':=inl), -> comp_assoc with (g':=inr), -> coprodhom_inr. |

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

1065 | |

1066 | |

1067 |
case_distinction. |

1068 |
case_distinction. |

1069 |
case_distinction. |

1070 | |

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

1072 |
rewrite <-2 comp_assoc with (h':=inl), -> comp_assoc with (g':=inl), -> coprodhom_inl. |

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

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

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

1076 |
trivial. |

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

1078 |
rewrite -> cpr_inr. |

1079 |
trivial. |

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

1081 |
rewrite ->3 comp_assoc, -> coprodhom_inl. |

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

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

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

1085 |
rewrite -> comp_assoc; trivial. |

1086 | |

1087 |
rewrite ->2 f_cpr. |

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

1089 |
rewrite -> cpr_inr. |

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

1091 |
rewrite <- f_cpr. |

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

1093 |
rewrite -> inl_inr_is_id. |

1094 |
rewrite -> mapc_id, -> cont_id, -> id_l. |

1095 |
trivial. |

1096 | |

1097 |
Qed. |

1098 | |

1099 | |

1100 | |

1101 |
Lemma delta : forall |

1102 |
(x x' y y' z z' a b : Obj) |

1103 |
(f: x ~> x') |

1104 |
(g: y ~> y') |

1105 |
(h: z ~> z'), |

1106 |
(f ×× g ⊕⊕ cont (f ×× h)) ∘ δ = δ ∘ (f ×× (g ⊕⊕ cont (a:=a) (b:=b) h)). |

1107 | |

1108 |
Proof. |

1109 |
intros. |

1110 |
unfold cont, δ. |

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

1112 |
rewrite ->2 comp_assoc with (f':=dist2); apply f_equal2; trivial. |

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

1114 |
apply f_equal2; trivial. |

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

1116 |
rewrite -> pair_f. |

1117 |
rewrite <- comp_assoc with (g':=pr2), -> pr2_prodhom. |

1118 |
rewrite -> comp_assoc with (h':=pr1), -> pr1_prodhom, -> id_r. |

1119 |
apply f_equal2; trivial. |

1120 |
rewrite -> curry2. |

1121 |
rewrite -> curry1. |

1122 |
apply f_equal1. |

1123 |
rewrite -> prodhom_pair. |

1124 |
rewrite -> pair_f. |

1125 |
rewrite <- comp_assoc with (g':=pr1), -> pr1_prodhom. |

1126 |
rewrite -> comp_assoc with (h':=pr1), -> pr1_prodhom. |

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

1128 |
rewrite <- uncurry1. |

1129 |
rewrite <- comp_assoc, -> pr2_prodhom. |

1130 |
rewrite -> comp_assoc, -> pr2_prodhom. |

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

1132 |
trivial. |

1133 |
Qed. |

1134 | |

1135 | |

1136 | |

1137 |
Lemma naturality_τv : forall |

1138 |
(x x' y y' a b : Obj) |

1139 |
(f: x ~> x') |

1140 |
(g: y ~> y'), |

1141 |
τv ∘ (f ×× mapc g) = mapc (f ×× g) ∘ τv (a:=a) (b:=b) (x:=x). |

1142 | |

1143 |
Proof. |

1144 |
Admitted. |

1145 | |

1146 | |

1147 | |

1148 |
Lemma p_assoc_delta : forall (x y z a b : Obj), |

1149 |
(p_assoc1 ⊕⊕ cont p_assoc1) ∘ δ = δ ∘ |

1150 |
((id ×× δ (y:=z) (z:=coext T a b z) (a:=a) (b:=b)) ∘ p_assoc1 (a:=x) (b:=y)). |

1151 | |

1152 |
Proof. |

1153 |
intros. |

1154 |
unfold δ at 1. |

1155 |
rewrite -> comp_assoc, -> coprodhom_comp, -> id_l. |

1156 |
unfold cont. |

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

1158 |
rewrite -> curry2. |

1159 |
unfold p_assoc1 at 2. |

1160 |
rewrite -> pair_f. |

1161 |
rewrite <- comp_assoc with (g':=pr1), -> pr1_pair. |

1162 |
rewrite -> pair_f. |

1163 |
rewrite <- comp_assoc with (g':=pr1), -> pr1_pair. |

1164 |
rewrite -> pr2_pair. |

1165 |
unfold dist2. |

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

1167 |
rewrite -> f_cpr. |

1168 |
rewrite ->2 curry2. |

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

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

1171 | |

1172 |
apply swapp_switch. |

1173 |
rewrite <- comp_assoc with (h':=δ); unfold p_assoc1 at 2. |

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

1175 |
unfold swapp at 3. |

1176 |
rewrite -> pair_f. |

1177 |
rewrite <- comp_assoc with (g':=pr1), -> pr1_pair. |

1178 |
rewrite <- comp_assoc with (h':=δ), -> pair_f. |

1179 |
rewrite <- comp_assoc with (g':=pr1), -> pr1_pair. |

1180 |
rewrite -> pr2_pair. |

1181 | |

1182 |
apply curry_cong. |

1183 |
rewrite -> curry_uncurry. |

1184 |
case_distinction. |

1185 | |

1186 |
rewrite -> cpr_inl. |

1187 |
rewrite -> curry1. |

1188 |
apply f_equal1. |

1189 |
rewrite <- comp_assoc with (h':=δ), -> pair_f. |

1190 |
rewrite <- comp_assoc with (g':=pr2), -> pr2_prodhom, -> id_r. |

1191 |
rewrite <- comp_assoc with (h':=δ), -> pair_f. |

1192 |
rewrite <- comp_assoc with (g':=pr2), -> pr2_prodhom, -> id_r. |

1193 |
rewrite -> pr1_prodhom. |

1194 | |

1195 |
unfold δ at 1. |

1196 |
rewrite <- comp_assoc with (g':=dist2); |

1197 |
unfold dist2. |

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

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

1200 |
rewrite -> f_cpr. |

1201 |
rewrite ->2 curry2. |

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

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

1204 | |

1205 |
assert (aux: swapp ∘ (inl ×× pr2) = pair (pr2 (a:=x) (b:=y) ∘ pr2) (inl (b:=a × coext T a b z ^ b) ∘ pr1 (a:=z))). |

1206 |
unfold prodhom, swapp. |

1207 |
rewrite -> pair_f. |

1208 |
rewrite -> pr2_pair, -> pr1_pair. |

1209 |
trivial. |

1210 |
rewrite <- aux; clear aux. |

1211 | |

1212 |
unfold δ. |

1213 |
unfold dist2. |

1214 |
rewrite -> comp_assoc with (g':=swapp), <-4 comp_assoc with (f':=swapp), |

1215 |
-> swapp_id, -> id_l. |

1216 | |

1217 |
assert (aux: (inl ×× id) ∘ (id ×× pr2) = inl (a:=z) (b:=a × coext T a b z ^ b) ×× pr2 (a:=x) (b:=y)). |

1218 |
rewrite -> prodhom_comp, -> id_l, -> id_r. |

1219 |
trivial. |

1220 |
rewrite <- aux; clear aux. |

1221 | |

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

1223 |
rewrite -> cpr_inl. |

1224 |
rewrite -> uncurry_curry. |

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

1226 | |

1227 |
assert (aux: (((inl ∘ swapp) ∘ (id ×× pr2)) ×× id) ∘ pair id (pr1 ∘ pr2) = |

1228 |
pair ((inl (b:=a × (y × coext T a b z) ^ b) ∘ swapp) ∘ (id ×× pr2)) (pr1 (a:=x) (b:=y) ∘ pr2 (a:=z))). |

1229 |
rewrite -> prodhom_pair, -> id_l, -> id_r. |

1230 |
trivial. |

1231 |
rewrite <- aux; clear aux. |

1232 | |

1233 |
rewrite ->2 comp_assoc, <- uncurry1. |

1234 |
rewrite ->2 comp_assoc, -> cpr_inl. |

1235 |
rewrite -> curry1. |

1236 |
rewrite -> curry1. |

1237 |
rewrite -> uncurry_curry. |

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

1239 |
rewrite <- comp_assoc with (h':=inl ∘ swapp), -> prodhom_pair, -> id_l, -> id_r. |

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

1241 |
rewrite <- comp_assoc; unfold p_assoc1. |

1242 |
rewrite ->2 pair_f. |

1243 |
unfold swapp. |

1244 |
rewrite <-2 comp_assoc with (g':=pr1), -> pr1_pair. |

1245 |
rewrite -> pr2_pair. |

1246 |
rewrite -> pair_f. |

1247 |
rewrite -> pr2_prodhom. |

1248 |
rewrite -> pr1_prodhom, -> id_r. |

1249 |
trivial. |

1250 | |

1251 | |

1252 |
(* analogous to the computation for inl *) |

1253 |
rewrite -> cpr_inr. |

1254 |
rewrite -> curry1. |

1255 |
apply f_equal1. |

1256 |
rewrite <- comp_assoc with (h':=δ), -> pair_f. |

1257 |
rewrite <- comp_assoc with (g':=pr2), -> pr2_prodhom, -> id_r. |

1258 |
rewrite <- comp_assoc with (h':=δ), -> pair_f. |

1259 |
rewrite <- comp_assoc with (g':=pr2), -> pr2_prodhom, -> id_r. |

1260 |
rewrite -> pr1_prodhom. |

1261 | |

1262 |
unfold δ at 1. |

1263 |
rewrite <- comp_assoc with (g':=dist2); |

1264 |
unfold dist2. |

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

1266 |
rewrite ->3 comp_assoc, <- uncurry2. |

1267 |
rewrite -> f_cpr. |

1268 |
rewrite ->2 curry2. |

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

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

1271 | |

1272 |
assert (aux: swapp ∘ (inr ×× pr2) = pair (pr2 (a:=x) (b:=y) ∘ pr2) (inr (a:=z) ∘ pr1 (a:=a × coext T a b z ^ b))). |

1273 |
unfold prodhom, swapp. |

1274 |
rewrite -> pair_f. |

1275 |
rewrite -> pr2_pair, -> pr1_pair. |

1276 |
trivial. |

1277 |
rewrite <- aux; clear aux. |

1278 | |

1279 |
unfold δ. |

1280 |
unfold dist2. |

1281 |
rewrite -> comp_assoc with (g':=swapp), <-4 comp_assoc with (f':=swapp), |

1282 |
-> swapp_id, -> id_l. |

1283 | |

1284 |
assert (aux: (inr ×× id) ∘ (id ×× pr2) = inr (a:=z) (b:=a × coext T a b z ^ b) ×× pr2 (a:=x) (b:=y)). |

1285 |
rewrite -> prodhom_comp, -> id_l, -> id_r. |

1286 |
trivial. |

1287 |
rewrite <- aux; clear aux. |

1288 | |

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

1290 |
rewrite -> cpr_inr. |

1291 |
rewrite -> uncurry_curry. |

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

1293 | |

1294 |
assert (aux: ((((inr ∘ (pair (pr1 ∘ pr2) (curry (pair (pr1 ∘ pr1) (uncurry (pr2 ∘ pr2)))))) |

1295 |
∘ swapp) ∘ (id ×× pr2)) ×× id) ∘ pair id (pr1 ∘ pr2) = |

1296 |
pair (((inr (a:=y × z) ∘ (pair (pr1 ∘ pr2) (curry (pair (pr1 ∘ pr1) (uncurry (b:=b) (c:=coext T a b z) (pr2 (a:=a) ∘ pr2)))))) |

1297 |
∘ swapp) ∘ (id ×× pr2)) (pr1 (a:=x) (b:=y) ∘ pr2)). |

1298 |
rewrite -> prodhom_pair, -> id_l, -> id_r. |

1299 |
trivial. |

1300 |
rewrite <- aux; clear aux. |

1301 | |

1302 |
rewrite ->2 comp_assoc, <- uncurry1. |

1303 |
rewrite ->3 comp_assoc, -> cpr_inr. |

1304 |
rewrite -> curry1. |

1305 |
rewrite -> curry1. |

1306 |
rewrite -> curry1. |

1307 |
rewrite -> uncurry_curry. |

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

1309 |
rewrite <- comp_assoc with (g':=swapp ∘ (id ×× pr2) ×× id), -> prodhom_pair, -> id_l, -> id_r. |

1310 | |

1311 |
rewrite <-3 comp_assoc with (h':=inr). |

1312 |
apply f_equal2; trivial. |

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

1314 |
rewrite <-4 comp_assoc, -> swap_pair. |

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

1316 | |

1317 |
apply prodsplit. |

1318 |
rewrite ->3 comp_assoc with (h':=pr1), ->2 pr1_pair. |

1319 |
rewrite <-2 comp_assoc with (g':=pr2), -> pr2_pair. |

1320 |
rewrite ->2 comp_assoc with (h':=pr1), -> pr1_pair. |

1321 |
rewrite -> swap_prodhom. |

1322 |
rewrite -> comp_assoc, <- comp_assoc with (f':=pr2 ×× id), -> pr2_prodhom, -> id_r. |

1323 |
trivial. |

1324 | |

1325 |
rewrite ->3 comp_assoc with (h':=pr2), ->2 pr2_pair. |

1326 |
rewrite ->2 curry1. |

1327 |
apply f_equal1. |

1328 |
rewrite ->2 pair_f. |

1329 |
rewrite <-3 comp_assoc with (f':=swapp ×× id), -> pr1_prodhom. |

1330 |
rewrite -> pair_f. |

1331 |
rewrite <-2 comp_assoc with (g':=pr1), -> pr1_prodhom. |

1332 |
rewrite ->3 comp_assoc with (h':=pr1), -> pr1_pair. |

1333 | |

1334 |
rewrite -> comp_assoc with (g':=swapp), <- comp_assoc with (f':=swapp); |

1335 |
unfold swapp at 1. |

1336 |
rewrite -> pr1_pair. |

1337 |
apply f_equal2;trivial. |

1338 | |

1339 |
rewrite <-2 uncurry1. |

1340 |
rewrite <-2 comp_assoc with (g':=pr2), -> pr2_pair. |

1341 |
rewrite ->4 comp_assoc with (h':=pr2), -> pr2_pair. |

1342 |
rewrite -> curry1. |

1343 |
rewrite -> uncurry_curry. |

1344 | |

1345 |
rewrite -> swap_prodhom. |

1346 |
rewrite -> pair_f. |

1347 |
rewrite <- comp_assoc with (h':=pr1), -> pr1_prodhom. |

1348 |
rewrite ->2 comp_assoc with (h':=pr1), -> pr1_prodhom. |

1349 |
apply f_equal2; trivial. |

1350 |
rewrite <- uncurry1. |

1351 |
apply f_equal1. |

1352 |
rewrite -> comp_assoc with (g':=pr2 ×× id), <- comp_assoc with (f':=pr2 ×× id), -> pr2_prodhom, -> id_r. |

1353 |
trivial. |

1354 | |

1355 |
Qed. |

1356 | |

1357 | |

1358 |
End Lemmas. |