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 _ }.
269 etransitivity. apply iso_id_lemma1. symmetry.
270 etransitivity. apply iso_id_lemma2. symmetry.
273 unfold garrow_functor.
274 unfold functor_comp at 1.
275 unfold functor_comp at 1.
276 Opaque functor_comp. simpl. Transparent functor_comp.
280 apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
281 unfold functor_comp at 1.
282 unfold functor_comp at 1.
283 Opaque functor_comp. simpl. Transparent functor_comp.
287 set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
288 unfold functor_comp in qq.
290 apply iso_shift_right' in qq.
291 apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
293 apply (me_faithful(MonicEnrichment:=CMon)).
297 set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
298 unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
299 set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
300 apply iso_shift_right' in zz'.
303 unfold functor_comp; simpl.
307 set full_roundtrip as full_roundtrip'.
308 unfold fmor in full_roundtrip'.
309 simpl in full_roundtrip'.
310 apply full_roundtrip'.
312 set (@iso_shift_right') as q. simpl in q. apply q. clear q.
314 set (@iso_shift_left) as q. simpl in q. apply q. clear q.
318 set full_roundtrip as full_roundtrip'.
319 unfold fmor in full_roundtrip'.
320 simpl in full_roundtrip'.
321 apply (fun a' b' f z => fmor_respects (bin_second(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
328 setoid_rewrite <- associativity.
329 setoid_rewrite <- associativity.
330 setoid_rewrite <- associativity.
331 setoid_rewrite <- associativity.
333 setoid_rewrite <- associativity.
337 eapply transitivity; [ idtac | apply right_identity ].
338 apply comp_respects; [ reflexivity | idtac ].
340 apply comp_respects; [ idtac | reflexivity ].
341 apply (mf_consistent(PreMonoidalFunctor:=CM)).
345 eapply comp_respects; [ idtac | reflexivity ].
346 eapply comp_respects; [ idtac | reflexivity ].
347 eapply comp_respects; [ idtac | reflexivity ].
348 eapply comp_respects; [ idtac | reflexivity ].
351 eapply associativity.
352 eapply transitivity; [ idtac | apply left_identity ].
353 eapply comp_respects; [ idtac | reflexivity ].
355 eapply comp_respects; [ idtac | reflexivity ].
357 apply (mf_consistent(PreMonoidalFunctor:=CM)).
362 setoid_rewrite <- fmor_preserves_comp.
363 setoid_rewrite <- fmor_preserves_comp.
367 apply comp_respects; try reflexivity.
377 apply comp_respects; try reflexivity.
380 eapply comp_respects; [ reflexivity | idtac ].
382 eapply comp_respects; [ idtac | reflexivity ].
385 eapply comp_respects; [ reflexivity | idtac ].
387 apply iso_comp1_right.
390 eapply comp_respects; [ reflexivity | idtac ].
393 eapply comp_respects; [ reflexivity | idtac ].
397 eapply transitivity; [ idtac | apply left_identity ].
398 eapply comp_respects; [ idtac | reflexivity ].
400 eapply comp_respects; [ idtac | reflexivity ].
402 eapply (mf_consistent(PreMonoidalFunctor:=reification)).
406 eapply comp_respects; [ reflexivity | idtac ].
408 apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
409 eapply transitivity; [ idtac | apply right_identity ].
415 eapply comp_respects; [ idtac | reflexivity ].
417 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
421 apply right_identity.
423 eapply transitivity; [ idtac | apply left_identity ].
424 apply comp_respects; [ idtac | reflexivity ].
428 eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
430 apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
434 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
435 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
436 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
438 Lemma assoc_coherent (a b c : enr_v K) :
439 (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
440 (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
441 #((garrow_second a) (b ⊗ c)) ~~
442 (#((garrow_second a) b) ⋉ garrow_functor c >>>
443 #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
446 eapply transitivity; [ idtac | apply right_identity ].
447 eapply comp_respects; [ eapply reflexivity | idtac ].
452 eapply transitivity; [ idtac | apply left_identity ].
453 eapply comp_respects; [ idtac | eapply reflexivity ].
454 eapply transitivity; [ idtac | apply right_identity ].
457 apply (fmor_preserves_id (ebc_first (garrow_functor c))).
462 eapply transitivity; [ idtac | apply right_identity ].
466 apply (fmor_preserves_id (ebc_second (garrow_functor a))).
470 unfold garrow_functor.
471 unfold step2_functor.
473 Opaque ff_functor_section_functor.
477 Transparent ff_functor_section_functor.
479 apply (me_faithful(MonicEnrichment:=CMon)).
480 eapply transitivity; [ eapply full_roundtrip | idtac ].
484 unfold me_homfunctor.
485 set (mf_assoc(PreMonoidalFunctor:=reification) a b c) as q.
486 set (mf_assoc(PreMonoidalFunctor:=CM) (garrow_fobj a) (garrow_fobj b) (garrow_fobj c)) as q'.
492 Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
493 iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
494 #((mf_first F b) _) >>> F \ #(pmon_cancell b).
495 set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
496 setoid_rewrite associativity in q.
497 set (@comp_respects) as qq.
499 unfold respectful in qq.
500 set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
501 setoid_rewrite <- associativity in q'.
503 setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
504 eapply transitivity; [ apply q' | idtac ].
506 setoid_rewrite <- associativity.
507 apply comp_respects; try reflexivity.
509 apply iso_shift_left.
510 setoid_rewrite iso_comp1.
512 eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
513 apply (fmor_respects (-⋉ F b)).
517 Lemma cancell_coherent (b:enr_v K) :
518 #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
519 (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
520 #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
524 setoid_rewrite right_identity.
526 eapply transitivity; [ idtac | apply left_identity ].
528 apply (fmor_preserves_id (ebc_first (garrow_functor b))).
529 unfold garrow_functor.
530 unfold step2_functor.
536 apply (me_faithful(MonicEnrichment:=CMon)).
537 eapply transitivity; [ eapply full_roundtrip | idtac ].
540 apply comp_respects; [ idtac | reflexivity ].
541 apply comp_respects; [ idtac | reflexivity ].
542 apply comp_respects; [ reflexivity | idtac ].
543 apply comp_respects; [ idtac | reflexivity ].
544 apply comp_respects; [ reflexivity | idtac ].
546 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
549 apply iso_shift_left.
555 apply comp_respects; [ reflexivity | idtac ].
560 apply comp_respects; [ reflexivity | idtac ].
563 apply comp_respects; [ reflexivity | idtac ].
565 set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
566 eapply transitivity; [ idtac | apply associativity ].
569 apply iso_shift_left'.
573 set (@iso_shift_right') as qq.
577 unfold me_homfunctor.
580 apply (cancell_lemma CM (garrow_fobj b)).
584 apply comp_respects; [ idtac | reflexivity ].
587 eapply associativity.
588 apply comp_respects; [ idtac | reflexivity ].
590 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
596 apply comp_respects; try reflexivity.
601 set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
606 apply comp_respects; [ idtac | reflexivity ].
614 eapply transitivity; [ idtac | apply right_identity ].
615 apply comp_respects; try reflexivity.
619 Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
620 (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
621 #((mf_first F _) _) >>> F \ #(pmon_cancelr b).
622 set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
623 setoid_rewrite associativity in q.
624 set (@comp_respects) as qq.
626 unfold respectful in qq.
627 set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
628 setoid_rewrite <- associativity in q'.
630 setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
631 eapply transitivity; [ apply q' | idtac ].
633 setoid_rewrite <- associativity.
634 apply comp_respects; try reflexivity.
636 apply iso_shift_left.
637 setoid_rewrite iso_comp1.
639 eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
640 apply (fmor_respects (-⋉ F b)).
644 Lemma cancelr_coherent (b:enr_v K) :
645 #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
646 (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
647 #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
651 setoid_rewrite right_identity.
653 eapply transitivity; [ idtac | apply left_identity ].
655 apply (fmor_preserves_id (ebc_second (garrow_functor b))).
656 unfold garrow_functor.
657 unfold step2_functor.
663 apply (me_faithful(MonicEnrichment:=CMon)).
664 eapply transitivity; [ eapply full_roundtrip | idtac ].
667 apply comp_respects; [ idtac | reflexivity ].
668 apply comp_respects; [ idtac | reflexivity ].
669 apply comp_respects; [ reflexivity | idtac ].
670 apply comp_respects; [ idtac | reflexivity ].
671 apply comp_respects; [ idtac | reflexivity ].
673 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
676 apply iso_shift_left.
682 apply comp_respects; [ reflexivity | idtac ].
686 set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
687 setoid_rewrite associativity in q.
693 apply comp_respects; [ reflexivity | idtac ].
698 apply comp_respects; [ idtac | reflexivity ].
700 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
703 apply comp_respects; [ reflexivity | idtac ].
705 apply comp_respects; [ reflexivity | idtac ].
706 apply comp_respects; [ idtac | reflexivity ].
711 apply iso_shift_left'.
715 set (@iso_shift_right') as qq.
719 unfold me_homfunctor.
722 apply (cancelr_lemma CM (garrow_fobj b)).
727 set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
730 apply comp_respects; [ idtac | reflexivity ].
731 apply comp_respects; [ reflexivity | idtac ].
738 apply comp_respects; try reflexivity.
743 eapply transitivity; [ idtac | apply right_identity ].
744 apply comp_respects; try reflexivity.
748 Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
749 { mf_first := garrow_first
750 ; mf_second := garrow_second
751 ; mf_i := iso_id _ }.
753 intros; apply (reification_host_lang_pure _ _ _ reification).
754 apply cancell_coherent.
755 apply cancelr_coherent.
756 apply assoc_coherent.
759 Definition garrow_from_reification : GeneralizedArrow K CM :=
760 {| ga_functor_monoidal := garrow_monoidal
761 ; ga_host_lang_pure := reification_host_lang_pure _ _ _ reification
764 End GArrowFromReification.