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 _ }.
271 Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
272 Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
273 Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
275 Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
276 iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
277 #((mf_first F b) _) >>> F \ #(pmon_cancell b).
278 set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
279 setoid_rewrite associativity in q.
280 set (@comp_respects) as qq.
282 unfold respectful in qq.
283 set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
284 setoid_rewrite <- associativity in q'.
286 setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
287 eapply transitivity; [ apply q' | idtac ].
289 setoid_rewrite <- associativity.
290 apply comp_respects; try reflexivity.
292 apply iso_shift_left.
293 setoid_rewrite iso_comp1.
295 eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
296 apply (fmor_respects (-⋉ F b)).
300 Lemma cancell_coherent (b:enr_v K) :
301 #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
302 (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
303 #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
307 setoid_rewrite right_identity.
309 eapply transitivity; [ idtac | apply left_identity ].
311 apply (fmor_preserves_id (ebc_first (garrow_functor b))).
312 unfold garrow_functor.
313 unfold step2_functor.
319 apply (me_faithful(MonicEnrichment:=CMon)).
320 eapply transitivity; [ eapply full_roundtrip | idtac ].
323 apply comp_respects; [ idtac | reflexivity ].
324 apply comp_respects; [ idtac | reflexivity ].
325 apply comp_respects; [ reflexivity | idtac ].
326 apply comp_respects; [ idtac | reflexivity ].
327 apply comp_respects; [ reflexivity | idtac ].
329 apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
332 apply iso_shift_left.
338 apply comp_respects; [ reflexivity | idtac ].
343 apply comp_respects; [ reflexivity | idtac ].
346 apply comp_respects; [ reflexivity | idtac ].
348 set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
349 eapply transitivity; [ idtac | apply associativity ].
352 apply iso_shift_left'.
356 set (@iso_shift_right') as qq.
360 unfold me_homfunctor.
363 apply (cancell_lemma CM (garrow_fobj b)).
367 apply comp_respects; [ idtac | reflexivity ].
370 eapply associativity.
371 apply comp_respects; [ idtac | reflexivity ].
373 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
379 apply comp_respects; try reflexivity.
384 set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
389 apply comp_respects; [ idtac | reflexivity ].
397 eapply transitivity; [ idtac | apply right_identity ].
398 apply comp_respects; try reflexivity.
402 Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
403 (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
404 #((mf_first F _) _) >>> F \ #(pmon_cancelr b).
405 set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
406 setoid_rewrite associativity in q.
407 set (@comp_respects) as qq.
409 unfold respectful in qq.
410 set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
411 setoid_rewrite <- associativity in q'.
413 setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
414 eapply transitivity; [ apply q' | idtac ].
416 setoid_rewrite <- associativity.
417 apply comp_respects; try reflexivity.
419 apply iso_shift_left.
420 setoid_rewrite iso_comp1.
422 eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
423 apply (fmor_respects (-⋉ F b)).
427 Lemma cancelr_coherent (b:enr_v K) :
428 #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
429 (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
430 #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
435 setoid_rewrite right_identity.
437 eapply transitivity; [ idtac | apply left_identity ].
439 apply (fmor_preserves_id (ebc_second (garrow_functor b))).
440 unfold garrow_functor.
441 unfold step2_functor.
447 apply (me_faithful(MonicEnrichment:=CMon)).
448 eapply transitivity; [ eapply full_roundtrip | idtac ].
451 apply comp_respects; [ idtac | reflexivity ].
452 apply comp_respects; [ idtac | reflexivity ].
453 apply comp_respects; [ reflexivity | idtac ].
454 apply comp_respects; [ idtac | reflexivity ].
455 apply comp_respects; [ idtac | reflexivity ].
457 apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
460 apply iso_shift_left.
466 apply comp_respects; [ reflexivity | idtac ].
470 set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
471 setoid_rewrite associativity in q.
477 apply comp_respects; [ reflexivity | idtac ].
482 apply comp_respects; [ idtac | reflexivity ].
484 eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
487 apply comp_respects; [ reflexivity | idtac ].
489 apply comp_respects; [ reflexivity | idtac ].
490 apply comp_respects; [ idtac | reflexivity ].
495 apply iso_shift_left'.
499 set (@iso_shift_right') as qq.
503 unfold me_homfunctor.
506 apply (cancelr_lemma CM (garrow_fobj b)).
511 set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
514 apply comp_respects; [ idtac | reflexivity ].
515 apply comp_respects; [ reflexivity | idtac ].
522 apply comp_respects; try reflexivity.
527 eapply transitivity; [ idtac | apply right_identity ].
528 apply comp_respects; try reflexivity.
532 Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
533 { mf_first := garrow_first
534 ; mf_second := garrow_second
535 ; mf_i := iso_id _ }.
538 unfold garrow_functor.
541 unfold step2_functor.
545 apply cancell_coherent.
546 apply cancelr_coherent.
550 Definition garrow_from_reification : GeneralizedArrow K CM :=
551 {| ga_functor_monoidal := garrow_monoidal |}.
553 End GArrowFromReification.