Project

General

Profile

Statistics
| Branch: | Revision:

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.