1 (*********************************************************************************************************************************)
2 (* GeneralizedArrowFromReification: *)
4 (* Turn a reification into a generalized arrow *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import Functors_ch1_4.
13 Require Import Isomorphisms_ch1_5.
14 Require Import ProductCategories_ch1_6_1.
15 Require Import OppositeCategories_ch1_6_2.
16 Require Import Enrichment_ch2_8.
17 Require Import Subcategories_ch7_1.
18 Require Import NaturalTransformations_ch7_4.
19 Require Import NaturalIsomorphisms_ch7_5.
20 Require Import BinoidalCategories.
21 Require Import PreMonoidalCategories.
22 Require Import PreMonoidalCenter.
23 Require Import MonoidalCategories_ch7_8.
24 Require Import Coherence_ch7_8.
25 Require Import Enrichment_ch2_8.
26 Require Import Enrichments.
27 Require Import RepresentableStructure_ch7_2.
28 Require Import Reification.
29 Require Import GeneralizedArrow.
31 Section GArrowFromReification.
33 Definition binoidalcat_iso `{bc:BinoidalCat}{a1 b1 a2 b2:bc} (i1:a1≅a2)(i2:b1≅b2) : (a1⊗b1)≅(a2⊗b2) :=
35 (functors_preserve_isos (- ⋉ b1) i1 )
36 (functors_preserve_isos (a2 ⋊ -) i2).
38 Context `(K : SurjectiveEnrichment)
39 `(CMon : MonicEnrichment C)
40 (CM : MonoidalEnrichment C)
41 (reification : Reification K C (pmon_I (enr_c_pm C))).
43 Fixpoint garrow_fobj (vk:senr_v K) : C :=
45 | T_Leaf None => enr_c_i C
46 | T_Leaf (Some a) => match a with (a1,a2) => reification_r reification a1 a2 end
47 | t1,,t2 => bin_obj(BinoidalCat:=enr_c_bin C) (garrow_fobj t1) (garrow_fobj t2)
50 Fixpoint homset_tensor_iso (vk:enr_v_mon K) : reification vk ≅ enr_c_i C ~~> garrow_fobj vk :=
51 match vk as VK return reification VK ≅ enr_c_i C ~~> garrow_fobj VK with
52 | T_Leaf None => (mf_i(PreMonoidalFunctor:=reification))⁻¹ >>≅>> (mf_i(PreMonoidalFunctor:=CM))
53 | T_Leaf (Some a) => match a as A
54 return reification (T_Leaf (Some A)) ≅ enr_c_i C ~~> garrow_fobj (T_Leaf (Some A)) with
55 (s,s0) => iso_inv _ _ (ni_iso (reification_commutes reification s) s0)
57 | t1,,t2 => (ni_iso (@mf_first _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ reification _) _)⁻¹ >>≅>>
58 (binoidalcat_iso (homset_tensor_iso t1) (homset_tensor_iso t2)) >>≅>>
59 (ni_iso (mf_first(PreMonoidalFunctor:=CM) (garrow_fobj t2)) _)
62 Definition HomFunctor_fullimage := FullImage CM.
64 (* R' is a functor from the domain of the reification functor
65 * to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
66 Instance R' : Functor (FullImage (reification_rstar reification)) HomFunctor_fullimage garrow_fobj :=
67 { fmor := fun a b (f:a~~{FullImage (reification_rstar reification)}~~>b) =>
68 (#(homset_tensor_iso a)⁻¹ >>> f >>> #(homset_tensor_iso b))
70 abstract (intros; simpl;
71 apply comp_respects; try reflexivity;
72 apply comp_respects; try reflexivity;
74 abstract (intros; simpl;
75 setoid_rewrite right_identity;
79 repeat setoid_rewrite <- associativity;
80 apply comp_respects; try reflexivity;
81 repeat setoid_rewrite associativity;
82 apply comp_respects; try apply reflexivity;
83 apply comp_respects; try apply reflexivity;
84 eapply transitivity; [ symmetry; apply associativity | idtac ];
85 eapply transitivity; [ idtac | apply left_identity ];
86 apply comp_respects; try apply reflexivity;
90 (* the "step2_functor" is the section of the Hom(I,-) functor *)
91 Definition step2_functor :=
92 ff_functor_section_functor _ (me_full(MonicEnrichment:=CMon)) (me_faithful(MonicEnrichment:=CMon)).
94 Definition garrow_functor :=
95 RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor).
97 Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f.
102 Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f.
104 apply right_identity.
107 Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f.
109 unfold ff_functor_section_fmor.
110 set (me_full a b f) as full.
115 Opaque UnderlyingFunctor.
116 Instance garrow_first a :
117 (garrow_functor >>>> bin_first(BinoidalCat:=enr_c_bin C) (R' a)) <~~~>
118 (bin_first(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
119 { ni_iso := fun a => iso_id _ }.
121 etransitivity. apply iso_id_lemma1. symmetry.
122 etransitivity. apply iso_id_lemma2. symmetry.
125 unfold garrow_functor.
126 unfold functor_comp at 1.
127 unfold functor_comp at 1.
128 Opaque functor_comp. simpl. Transparent functor_comp.
132 apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_first (R' a)) f).
133 unfold functor_comp at 1.
134 unfold functor_comp at 1.
135 Opaque functor_comp. simpl. Transparent functor_comp.
139 set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
140 unfold functor_comp in qq.
142 apply iso_shift_right' in qq.
143 apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
145 apply (me_faithful(MonicEnrichment:=CMon)).
149 set (ni_commutes (mf_first(PreMonoidalFunctor:=CM) (R' a))) as zz.
150 unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
151 set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
152 apply iso_shift_right' in zz'.
155 unfold functor_comp; simpl.
159 set full_roundtrip as full_roundtrip'.
160 unfold fmor in full_roundtrip'.
161 simpl in full_roundtrip'.
162 apply full_roundtrip'.
164 set (@iso_shift_right') as q. simpl in q. apply q. clear q.
166 set (@iso_shift_left) as q. simpl in q. apply q. clear q.
170 set full_roundtrip as full_roundtrip'.
171 unfold fmor in full_roundtrip'.
172 simpl in full_roundtrip'.
173 apply (fun a' b' f z => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
180 setoid_rewrite <- associativity.
181 setoid_rewrite <- associativity.
182 setoid_rewrite <- associativity.
183 setoid_rewrite <- associativity.
185 setoid_rewrite <- associativity.
187 apply iso_comp1_left.
190 eapply comp_respects; [ idtac | reflexivity ].
191 eapply comp_respects; [ idtac | reflexivity ].
192 eapply comp_respects; [ idtac | reflexivity ].
193 eapply comp_respects; [ idtac | reflexivity ].
194 apply iso_comp1_right.
198 setoid_rewrite <- fmor_preserves_comp.
199 setoid_rewrite <- fmor_preserves_comp.
206 eapply comp_respects; [ reflexivity | idtac ].
207 apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
211 apply comp_respects; try apply reflexivity.
214 eapply comp_respects; [ idtac | reflexivity ].
215 eapply comp_respects; [ idtac | reflexivity ].
217 eapply associativity.
219 eapply comp_respects; [ idtac | reflexivity ].
220 eapply comp_respects; [ idtac | reflexivity ].
221 eapply comp_respects; [ idtac | reflexivity ].
222 apply iso_comp1_left.
225 eapply comp_respects; [ idtac | reflexivity ].
227 eapply comp_respects.
229 eapply associativity.
231 apply iso_comp1_left.
234 eapply comp_respects; [ idtac | reflexivity ].
235 eapply comp_respects; [ idtac | reflexivity ].
237 apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
239 eapply comp_respects; [ idtac | reflexivity ].
242 eapply comp_respects; [ reflexivity | idtac ].
244 apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
248 eapply comp_respects; [ reflexivity | idtac ].
251 eapply transitivity; [ idtac | apply right_identity ].
252 eapply comp_respects; [ reflexivity | idtac ].
255 apply fmor_preserves_comp.
256 setoid_rewrite iso_comp2.
257 apply fmor_preserves_id.
264 Instance garrow_second a :
265 (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
266 <~~~> (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
267 { ni_iso := fun a => iso_id _ }.
270 etransitivity. apply iso_id_lemma1. symmetry.
271 etransitivity. apply iso_id_lemma2. symmetry.
274 unfold garrow_functor.
275 unfold functor_comp at 1.
276 unfold functor_comp at 1.
277 Opaque functor_comp. simpl. Transparent functor_comp.
281 apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
282 unfold functor_comp at 1.
283 unfold functor_comp at 1.
284 Opaque functor_comp. simpl. Transparent functor_comp.
288 set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
289 unfold functor_comp in qq.
291 apply iso_shift_right' in qq.
292 apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
294 apply (me_faithful(MonicEnrichment:=CMon)).
298 set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
299 unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
300 set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
301 apply iso_shift_right' in zz'.
304 unfold functor_comp; simpl.
308 set full_roundtrip as full_roundtrip'.
309 unfold fmor in full_roundtrip'.
310 simpl in full_roundtrip'.
311 apply full_roundtrip'.
313 set (@iso_shift_right') as q. simpl in q. apply q. clear q.
315 set (@iso_shift_left) as q. simpl in q. apply q. clear q.
319 set full_roundtrip as full_roundtrip'.
320 unfold fmor in full_roundtrip'.
321 simpl in full_roundtrip'.
322 apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
329 setoid_rewrite <- associativity.
330 setoid_rewrite <- associativity.
331 setoid_rewrite <- associativity.
332 setoid_rewrite <- associativity.
334 setoid_rewrite <- associativity.
338 eapply transitivity; [ idtac | apply right_identity ].
339 apply comp_respects; [ reflexivity | idtac ].
341 apply comp_respects; [ idtac | reflexivity ].
342 apply (mf_consistent(PreMonoidalFunctor:=CM)).
346 eapply comp_respects; [ idtac | reflexivity ].
347 eapply comp_respects; [ idtac | reflexivity ].
348 eapply comp_respects; [ idtac | reflexivity ].
349 eapply comp_respects; [ idtac | reflexivity ].
352 eapply associativity.
353 eapply transitivity; [ idtac | apply left_identity ].
354 eapply comp_respects; [ idtac | reflexivity ].
356 eapply comp_respects; [ idtac | reflexivity ].
358 apply (mf_consistent(PreMonoidalFunctor:=CM)).
363 setoid_rewrite <- fmor_preserves_comp.
364 setoid_rewrite <- fmor_preserves_comp.
368 apply comp_respects; try reflexivity.
378 apply comp_respects; try reflexivity.
381 eapply comp_respects; [ reflexivity | idtac ].
383 eapply comp_respects; [ idtac | reflexivity ].
386 eapply comp_respects; [ reflexivity | idtac ].
388 apply iso_comp1_right.
391 eapply comp_respects; [ reflexivity | idtac ].
394 eapply comp_respects; [ reflexivity | idtac ].
398 eapply transitivity; [ idtac | apply left_identity ].
399 eapply comp_respects; [ idtac | reflexivity ].
401 eapply comp_respects; [ idtac | reflexivity ].
403 eapply (mf_consistent(PreMonoidalFunctor:=reification)).
407 eapply comp_respects; [ reflexivity | idtac ].
409 apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
410 eapply transitivity; [ idtac | apply right_identity ].
416 eapply comp_respects; [ idtac | reflexivity ].
418 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
422 apply right_identity.
424 eapply transitivity; [ idtac | apply left_identity ].
425 apply comp_respects; [ idtac | reflexivity ].
429 eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
431 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
435 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
436 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
437 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
439 Lemma assoc_lemma1 : forall a b c,
440 iso_backward ((mf_first reification c) (a ⊗ b)) >>>
441 iso_backward ((mf_second reification a) b) ⋉ reification c >>>
442 #(pmon_assoc(PreMonoidalCat:=enr_v_mon C) (reification a) (reification c) (reification_rstar_obj reification b)) >>>
443 reification a ⋊ #((mf_first reification c) b) >>>
444 #((mf_second reification a) (b ⊗ c)) ~~
445 reification \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
455 set (@iso_shift_right') as q.
462 apply comp_respects; [ reflexivity | idtac ].
463 set (mf_assoc(PreMonoidalFunctor:=reification)) as q.
472 apply comp_respects; try reflexivity.
476 eapply transitivity; [ idtac | apply left_identity ].
477 apply comp_respects; try reflexivity.
480 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
481 eapply transitivity; [ idtac |
482 apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
483 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
487 Lemma assoc_lemma2 : forall a b c,
488 iso_backward ((mf_first CM (garrow_fobj c)) _) >>>
489 (bin_first(BinoidalCat:=enr_v_bin C) _ \ iso_backward ((mf_second CM (garrow_fobj a)) (garrow_fobj b))) >>>
490 (#((pmon_assoc(PreMonoidalCat:=enr_v_mon C) _ _) _) >>>
491 (bin_second(BinoidalCat:=enr_v_bin C) _ \
492 #((mf_first CM (garrow_fobj c)) (garrow_fobj b)))) >>>
493 #((mf_second CM (garrow_fobj a)) _) ~~
494 HomFunctor C _ \ #((pmon_assoc(PreMonoidalCat:=enr_c_pm C) (garrow_fobj a) (garrow_fobj c)) (garrow_fobj b)).
500 set (@iso_shift_right') as q.
508 apply comp_respects; [ reflexivity | idtac ].
509 set (mf_assoc(PreMonoidalFunctor:=CM)) as q.
515 apply comp_respects; try reflexivity.
519 eapply transitivity; [ idtac | apply left_identity ].
520 apply comp_respects; try reflexivity.
523 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
524 eapply transitivity; [ idtac |
525 apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
526 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
530 Lemma assoc_coherent (a b c : enr_v K) :
531 (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
532 (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
533 #((garrow_second a) (b ⊗ c)) ~~
534 (#((garrow_second a) b) ⋉ garrow_functor c >>>
535 #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
538 eapply transitivity; [ idtac | apply right_identity ].
539 eapply comp_respects; [ eapply reflexivity | idtac ].
544 eapply transitivity; [ idtac | apply left_identity ].
545 eapply comp_respects; [ idtac | eapply reflexivity ].
546 eapply transitivity; [ idtac | apply right_identity ].
549 apply (fmor_preserves_id (ebc_first (garrow_functor c))).
554 eapply transitivity; [ idtac | apply right_identity ].
558 apply (fmor_preserves_id (ebc_second (garrow_functor a))).
562 unfold garrow_functor.
563 unfold step2_functor.
565 Opaque ff_functor_section_functor.
569 Transparent ff_functor_section_functor.
571 apply (me_faithful(MonicEnrichment:=CMon)).
572 eapply transitivity; [ eapply full_roundtrip | idtac ].
576 unfold me_homfunctor.
578 eapply comp_respects; [ idtac | apply reflexivity ].
579 eapply comp_respects; [ apply reflexivity | idtac ].
590 eapply comp_respects; [ apply reflexivity | idtac ].
592 eapply (mf_consistent(PreMonoidalFunctor:=CM)).
597 apply comp_respects; [ idtac | apply reflexivity ].
606 apply comp_respects; [ reflexivity | idtac ].
610 apply comp_respects; [ reflexivity | idtac ].
615 apply comp_respects; [ idtac | reflexivity ].
620 apply comp_respects; [ reflexivity | idtac ].
621 apply comp_respects; [ idtac | reflexivity ].
623 apply (mf_consistent(PreMonoidalFunctor:=reification)).
624 apply comp_respects; [ reflexivity | idtac ].
626 apply right_identity.
631 apply comp_respects; [ idtac | reflexivity ].
634 apply comp_respects; [ reflexivity | idtac ].
636 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
639 apply comp_respects; [ reflexivity | idtac ].
642 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
643 apply comp_respects; [ idtac | reflexivity ].
645 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
646 apply comp_respects; [ reflexivity | idtac ].
651 apply comp_respects; [ idtac | reflexivity ].
655 apply comp_respects; [ reflexivity | idtac ].
658 eapply transitivity; [ idtac | apply right_identity ].
659 apply comp_respects; [ reflexivity | idtac ].
661 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
662 eapply transitivity; [ idtac |
663 apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_mon C) _)) ].
664 apply (fmor_respects (bin_second(BinoidalCat:=enr_v_mon C) _)).
678 apply comp_respects; [ idtac | reflexivity ].
682 apply comp_respects; [ idtac | reflexivity ].
685 apply comp_respects; [ reflexivity | idtac ].
689 apply comp_respects; [ idtac | reflexivity ].
691 apply comp_respects; [ reflexivity | idtac ].
693 apply iso_comp1_right.
696 apply comp_respects; [ idtac | reflexivity ].
698 apply comp_respects; [ reflexivity | idtac ].
703 apply comp_respects; [ idtac | reflexivity ].
705 apply comp_respects; [ idtac | reflexivity ].
707 apply comp_respects; [ reflexivity | idtac ].
710 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
712 apply comp_respects; [ reflexivity | idtac ].
714 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
721 apply comp_respects; [ idtac | reflexivity ].
722 apply comp_respects; [ idtac | reflexivity ].
725 eapply transitivity; [ idtac | apply right_identity ].
726 apply comp_respects; [ reflexivity | idtac ].
728 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
729 eapply transitivity; [ idtac | apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_mon C) _)) ].
730 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_mon C) _)).
732 apply comp_respects; [ idtac | reflexivity ].
733 eapply mf_consistent.
739 apply comp_respects; [ idtac | reflexivity ].
743 apply comp_respects; [ idtac | reflexivity ].
745 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
750 set (fun a b => isos_forward_equal_then_backward_equal _ _ (mf_consistent(PreMonoidalFunctor:=CM) a b)) as q.
753 apply comp_respects; [ idtac | reflexivity ].
754 set (q (garrow_fobj b) (garrow_fobj a)) as q'.
756 set (fun qq => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) qq) _ _ q') as q''.
759 apply comp_respects; [ reflexivity | idtac ].
763 apply comp_respects; [ reflexivity | idtac ].
764 apply comp_respects; [ reflexivity | idtac ].
765 apply comp_respects; [ idtac | reflexivity ].
766 set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c))
767 #(homset_tensor_iso a)) as xx.
768 unfold functor_comp in xx.
770 set (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C) (reification a) (reification b) (reification c)) as yy.
771 set (isos_forward_equal_then_backward_equal _ _ yy) as yy'.
773 apply comp_respects; [ idtac | reflexivity ].
774 apply symmetry in yy'.
775 eapply transitivity; [ idtac | apply yy' ].
779 apply iso_shift_right' in xx.
780 apply symmetry in xx.
782 assert (#((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) (reification a)) ⁻¹ >>>
783 #(homset_tensor_iso a) ⋉ (reification b ⊗ reification c)
785 (#(homset_tensor_iso a) ⋉ reification b) ⋉ reification c >>>
786 #((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) _)⁻¹).
787 apply iso_shift_left.
794 apply comp_respects; [ reflexivity | idtac ].
796 apply comp_respects; [ idtac | reflexivity ].
798 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_mon C) _)).
801 apply comp_respects; [ reflexivity | idtac ].
805 apply comp_respects; [ idtac | reflexivity ].
809 eapply transitivity; [ idtac | apply left_identity ].
810 apply comp_respects; [ idtac | reflexivity ].
812 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
813 eapply transitivity; [ idtac |
814 apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
815 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
817 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
818 eapply transitivity; [ idtac |
819 apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
820 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
823 set (fun a' => ni_commutes (pmon_assoc(PreMonoidalCat:=enr_v_mon C) a' (reification c))
824 (iso_backward (homset_tensor_iso b))) as xx.
825 unfold fmor in xx; unfold functor_comp in xx; simpl in xx.
827 apply comp_respects; [ reflexivity | idtac ].
830 eapply associativity.
831 apply comp_respects; [ idtac | reflexivity ].
833 apply comp_respects; [ reflexivity | idtac ].
835 eapply isos_forward_equal_then_backward_equal.
836 apply (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C)).
842 apply comp_respects; [ reflexivity | idtac ].
844 eapply associativity.
845 apply comp_respects; [ reflexivity | idtac ].
847 apply comp_respects; [ reflexivity | idtac ].
849 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
852 eapply associativity.
853 eapply transitivity; [ idtac | apply left_identity ].
854 apply comp_respects; [ idtac | reflexivity ].
856 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
857 eapply transitivity; [ idtac |
858 apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
861 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
862 eapply transitivity; [ idtac |
863 apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
864 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
867 set (fun a b => ni_commutes (pmon_assoc_ll(PreMonoidalCat:=enr_v_mon C) a b)) as xx.
868 unfold functor_comp in xx.
871 apply comp_respects; [ reflexivity | idtac ].
873 apply comp_respects; [ idtac | reflexivity ].
875 apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
883 apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
885 eapply transitivity; [ idtac | apply left_identity ].
886 apply comp_respects; [ idtac | reflexivity ].
888 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
889 eapply transitivity; [ idtac |
890 apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
895 Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
896 iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
897 #((mf_first F b) _) >>> F \ #(pmon_cancell b).
898 set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
899 setoid_rewrite associativity in q.
900 set (@comp_respects) as qq.
902 unfold respectful in qq.
903 set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
904 setoid_rewrite <- associativity in q'.
906 setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
907 eapply transitivity; [ apply q' | idtac ].
909 setoid_rewrite <- associativity.
910 apply comp_respects; try reflexivity.
912 apply iso_shift_left.
913 setoid_rewrite iso_comp1.
915 eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
916 apply (fmor_respects (-⋉ F b)).
920 Lemma cancell_coherent (b:enr_v K) :
921 #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
922 (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
923 #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
927 setoid_rewrite right_identity.
929 eapply transitivity; [ idtac | apply left_identity ].
931 apply (fmor_preserves_id (ebc_first (garrow_functor b))).
932 unfold garrow_functor.
933 unfold step2_functor.
939 apply (me_faithful(MonicEnrichment:=CMon)).
940 eapply transitivity; [ eapply full_roundtrip | idtac ].
943 apply comp_respects; [ idtac | reflexivity ].
944 apply comp_respects; [ idtac | reflexivity ].
945 apply comp_respects; [ reflexivity | idtac ].
946 apply comp_respects; [ idtac | reflexivity ].
947 apply comp_respects; [ reflexivity | idtac ].
949 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
952 apply iso_shift_left.
958 apply comp_respects; [ reflexivity | idtac ].
963 apply comp_respects; [ reflexivity | idtac ].
966 apply comp_respects; [ reflexivity | idtac ].
968 set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
969 eapply transitivity; [ idtac | apply associativity ].
972 apply iso_shift_left'.
976 set (@iso_shift_right') as qq.
980 unfold me_homfunctor.
983 apply (cancell_lemma CM (garrow_fobj b)).
987 apply comp_respects; [ idtac | reflexivity ].
990 eapply associativity.
991 apply comp_respects; [ idtac | reflexivity ].
993 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
999 apply comp_respects; try reflexivity.
1001 unfold functor_fobj.
1004 set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
1005 eapply transitivity.
1007 apply associativity.
1008 eapply transitivity.
1009 apply comp_respects; [ idtac | reflexivity ].
1015 eapply transitivity.
1016 apply associativity.
1017 eapply transitivity; [ idtac | apply right_identity ].
1018 apply comp_respects; try reflexivity.
1022 Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
1023 (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
1024 #((mf_first F _) _) >>> F \ #(pmon_cancelr b).
1025 set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
1026 setoid_rewrite associativity in q.
1027 set (@comp_respects) as qq.
1028 unfold Proper in qq.
1029 unfold respectful in qq.
1030 set (qq _ _ _ _ _ _ (F b ⋊ iso_backward (mf_i F)) (F b ⋊ iso_backward (mf_i F)) (reflexivity _) _ _ q) as q'.
1031 setoid_rewrite <- associativity in q'.
1033 setoid_rewrite (fmor_preserves_comp (F b ⋊ -)) in q'.
1034 eapply transitivity; [ apply q' | idtac ].
1036 setoid_rewrite <- associativity.
1037 apply comp_respects; try reflexivity.
1039 apply iso_shift_left.
1040 eapply transitivity.
1041 apply comp_respects; [ idtac | reflexivity ].
1042 apply mf_consistent.
1043 setoid_rewrite iso_comp1.
1045 eapply transitivity; [ idtac | eapply (fmor_preserves_id (F b ⋊ - ))].
1046 apply (fmor_respects (F b ⋊ -)).
1050 Lemma cancelr_coherent (b:enr_v K) :
1051 #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
1052 (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
1053 #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
1057 setoid_rewrite right_identity.
1059 eapply transitivity; [ idtac | apply left_identity ].
1060 apply comp_respects.
1061 apply (fmor_preserves_id (ebc_second (garrow_functor b))).
1062 unfold garrow_functor.
1063 unfold step2_functor.
1065 unfold functor_fobj.
1066 unfold functor_comp.
1069 apply (me_faithful(MonicEnrichment:=CMon)).
1070 eapply transitivity; [ eapply full_roundtrip | idtac ].
1072 eapply transitivity.
1073 apply comp_respects; [ idtac | reflexivity ].
1074 apply comp_respects; [ idtac | reflexivity ].
1075 apply comp_respects; [ reflexivity | idtac ].
1076 apply comp_respects; [ idtac | reflexivity ].
1077 apply comp_respects; [ idtac | reflexivity ].
1079 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
1082 apply iso_shift_left.
1085 eapply transitivity.
1086 eapply transitivity.
1087 apply associativity.
1088 apply comp_respects; [ reflexivity | idtac ].
1089 eapply transitivity.
1090 apply associativity.
1092 set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
1093 setoid_rewrite associativity in q.
1095 eapply transitivity.
1096 apply associativity.
1097 eapply transitivity.
1098 apply associativity.
1099 apply comp_respects; [ reflexivity | idtac ].
1100 eapply transitivity.
1102 apply associativity.
1103 eapply transitivity.
1104 apply comp_respects; [ idtac | reflexivity ].
1106 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
1107 eapply transitivity.
1108 apply associativity.
1109 apply comp_respects; [ reflexivity | idtac ].
1110 eapply transitivity.
1111 apply comp_respects; [ reflexivity | idtac ].
1112 apply comp_respects; [ idtac | reflexivity ].
1113 apply mf_consistent.
1117 apply iso_shift_left'.
1118 eapply transitivity.
1119 apply associativity.
1121 set (@iso_shift_right') as qq.
1125 unfold me_homfunctor.
1126 eapply transitivity.
1128 apply (cancelr_lemma CM (garrow_fobj b)).
1130 unfold functor_fobj.
1133 set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
1135 eapply transitivity.
1136 apply comp_respects; [ idtac | reflexivity ].
1137 apply comp_respects; [ reflexivity | idtac ].
1142 eapply transitivity.
1143 apply associativity.
1144 apply comp_respects; try reflexivity.
1147 eapply transitivity.
1148 apply associativity.
1149 eapply transitivity; [ idtac | apply right_identity ].
1150 apply comp_respects; try reflexivity.
1154 Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
1155 { mf_first := garrow_first
1156 ; mf_second := garrow_second
1157 ; mf_i := iso_id _ }.
1158 intros; reflexivity.
1159 intros; apply (reification_host_lang_pure _ _ _ reification).
1160 apply cancell_coherent.
1161 apply cancelr_coherent.
1162 apply assoc_coherent.
1165 Definition garrow_from_reification : GeneralizedArrow K C :=
1166 {| ga_functor_monoidal := garrow_monoidal
1167 ; ga_host_lang_pure := reification_host_lang_pure _ _ _ reification
1170 End GArrowFromReification.