src/GeneralizedArrowFromReification.v

   1 (*********************************************************************************************************************************)
   2 (* GeneralizedArrowFromReification:                                                                                              *)
   3 (*                                                                                                                               *)
   4 (*   Turn a reification into a generalized arrow                                                                                 *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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.
  30
  31 Section GArrowFromReification.
  32
  33   Definition binoidalcat_iso `{bc:BinoidalCat}{a1 b1 a2 b2:bc} (i1:a1≅a2)(i2:b1≅b2) : (a1⊗b1)≅(a2⊗b2) :=
  34     iso_comp
  35       (functors_preserve_isos (- ⋉ b1) i1 )
  36       (functors_preserve_isos (a2 ⋊ -) i2).
  37
  38   Context  `(K           : SurjectiveEnrichment)
  39            `(CMon        : MonicEnrichment C)
  40             (CM          : MonoidalEnrichment C)
  41             (reification : Reification K C (pmon_I (enr_c_pm C))).
  42
  43   Fixpoint garrow_fobj (vk:senr_v K) : C :=
  44     match vk with
  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)
  48     end.
  49
  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)
  56                          end
  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)) _)
  60     end.
  61
  62   Definition HomFunctor_fullimage := FullImage CM.
  63
  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))
  69     }.
  70     abstract (intros; simpl;
  71               apply comp_respects; try reflexivity;
  72               apply comp_respects; try reflexivity;
  73               auto).
  74     abstract (intros; simpl;
  75       setoid_rewrite right_identity;
  76       apply iso_comp2).
  77     abstract (intros;
  78       simpl;
  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;
  87       apply iso_comp1).
  88       Defined.
  89
  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)).
  93
  94   Definition garrow_functor :=
  95     RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor).
  96
  97   Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f.
  98     simpl.
  99     apply left_identity.
 100     Qed.
 101
 102   Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f.
 103     simpl.
 104     apply right_identity.
 105     Qed.
 106
 107   Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f.
 108     intros.
 109     unfold ff_functor_section_fmor.
 110     set (me_full a b f) as full.
 111     destruct full.
 112     apply e.
 113     Qed.
 114
 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 _ }.
 120     intros.
 121       etransitivity.  apply iso_id_lemma1.  symmetry.
 122       etransitivity.  apply iso_id_lemma2.  symmetry.
 123
 124     Opaque Underlying.
 125     unfold garrow_functor.
 126       unfold functor_comp at 1.
 127       unfold functor_comp at 1.
 128       Opaque functor_comp. simpl. Transparent functor_comp.
 129
 130     symmetry.
 131       eapply transitivity.
 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.
 136
 137     symmetry.
 138       eapply transitivity.
 139       set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
 140       unfold functor_comp in qq.
 141       simpl in qq.
 142       apply iso_shift_right' in qq.
 143       apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
 144
 145     apply (me_faithful(MonicEnrichment:=CMon)).
 146       symmetry.
 147       unfold fmor at 1.
 148       eapply transitivity.
 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'.
 153       apply zz'.
 154
 155     unfold functor_comp; simpl.
 156
 157     symmetry.
 158       eapply transitivity.
 159       set full_roundtrip as full_roundtrip'.
 160       unfold fmor in full_roundtrip'.
 161       simpl in full_roundtrip'.
 162       apply full_roundtrip'.
 163
 164     set (@iso_shift_right') as q. simpl in q. apply q. clear q.
 165
 166     set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
 167
 168     symmetry.
 169       eapply transitivity.
 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)).
 174       symmetry.
 175
 176     intros.
 177       unfold bin_obj.
 178       unfold senr_v_bobj.
 179
 180     setoid_rewrite <- associativity.
 181       setoid_rewrite <- associativity.
 182       setoid_rewrite <- associativity.
 183       setoid_rewrite <- associativity.
 184       simpl.
 185       setoid_rewrite <- associativity.
 186       etransitivity.
 187       apply iso_comp1_left.
 188
 189     eapply transitivity.
 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.
 195
 196     eapply symmetry.
 197       eapply transitivity.
 198       setoid_rewrite <- fmor_preserves_comp.
 199       setoid_rewrite <- fmor_preserves_comp.
 200       eapply reflexivity.
 201       eapply symmetry.
 202
 203     eapply transitivity.
 204       apply associativity.
 205       eapply transitivity.
 206       eapply comp_respects; [ reflexivity | idtac ].
 207       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 208       eapply transitivity.
 209       eapply symmetry.
 210       apply associativity.
 211       apply comp_respects; try apply reflexivity.
 212
 213     eapply transitivity.
 214       eapply comp_respects; [ idtac | reflexivity ].
 215       eapply comp_respects; [ idtac | reflexivity ].
 216       eapply symmetry.
 217       eapply associativity.
 218       eapply transitivity.
 219       eapply comp_respects; [ idtac | reflexivity ].
 220       eapply comp_respects; [ idtac | reflexivity ].
 221       eapply comp_respects; [ idtac | reflexivity ].
 222       apply iso_comp1_left.
 223
 224     eapply transitivity.
 225       eapply comp_respects; [ idtac | reflexivity ].
 226       eapply transitivity.
 227       eapply comp_respects.
 228       eapply symmetry.
 229       eapply associativity.
 230       eapply reflexivity.
 231       apply iso_comp1_left.
 232
 233     eapply transitivity.
 234       eapply comp_respects; [ idtac | reflexivity ].
 235       eapply comp_respects; [ idtac | reflexivity ].
 236       eapply symmetry.
 237       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 238       eapply transitivity.
 239       eapply comp_respects; [ idtac | reflexivity ].
 240       eapply transitivity.
 241       apply associativity.
 242       eapply comp_respects; [ reflexivity | idtac ].
 243       eapply symmetry.
 244       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 245       eapply transitivity.
 246       eapply transitivity.
 247       apply associativity.
 248       eapply comp_respects; [ reflexivity | idtac ].
 249       eapply transitivity.
 250       apply associativity.
 251       eapply transitivity; [ idtac | apply right_identity ].
 252       eapply comp_respects; [ reflexivity | idtac ].
 253       eapply transitivity.
 254       unfold functor_fobj.
 255       apply fmor_preserves_comp.
 256       setoid_rewrite iso_comp2.
 257       apply fmor_preserves_id.
 258
 259     apply comp_respects.
 260       reflexivity.
 261       reflexivity.
 262       Defined.
 263
 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 _ }.
 268
 269     intros.
 270       etransitivity.  apply iso_id_lemma1.  symmetry.
 271       etransitivity.  apply iso_id_lemma2.  symmetry.
 272
 273     Opaque Underlying.
 274     unfold garrow_functor.
 275       unfold functor_comp at 1.
 276       unfold functor_comp at 1.
 277       Opaque functor_comp. simpl. Transparent functor_comp.
 278
 279     symmetry.
 280       eapply transitivity.
 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.
 285
 286     symmetry.
 287       eapply transitivity.
 288       set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
 289       unfold functor_comp in qq.
 290       simpl in qq.
 291       apply iso_shift_right' in qq.
 292       apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
 293
 294     apply (me_faithful(MonicEnrichment:=CMon)).
 295       symmetry.
 296       unfold fmor at 1.
 297       eapply transitivity.
 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'.
 302       apply zz'.
 303
 304     unfold functor_comp; simpl.
 305
 306     symmetry.
 307       eapply transitivity.
 308       set full_roundtrip as full_roundtrip'.
 309       unfold fmor in full_roundtrip'.
 310       simpl in full_roundtrip'.
 311       apply full_roundtrip'.
 312
 313     set (@iso_shift_right') as q. simpl in q. apply q. clear q.
 314
 315     set (@iso_shift_left) as q.   simpl in q. apply q. clear q.
 316
 317     symmetry.
 318       eapply transitivity.
 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)).
 323       symmetry.
 324
 325     intros.
 326       unfold bin_obj.
 327       unfold senr_v_bobj.
 328
 329     setoid_rewrite <- associativity.
 330       setoid_rewrite <- associativity.
 331       setoid_rewrite <- associativity.
 332       setoid_rewrite <- associativity.
 333       simpl.
 334       setoid_rewrite <- associativity.
 335       etransitivity.
 336       eapply transitivity.
 337         apply associativity.
 338         eapply transitivity; [ idtac | apply right_identity ].
 339         apply comp_respects; [ reflexivity | idtac ].
 340         etransitivity.
 341         apply comp_respects; [ idtac | reflexivity ].
 342         apply (mf_consistent(PreMonoidalFunctor:=CM)).
 343         apply iso_comp1.
 344
 345     eapply transitivity.
 346       eapply comp_respects; [ idtac | reflexivity ].
 347       eapply comp_respects; [ idtac | reflexivity ].
 348       eapply comp_respects; [ idtac | reflexivity ].
 349       eapply comp_respects; [ idtac | reflexivity ].
 350       eapply transitivity.
 351         eapply symmetry.
 352         eapply associativity.
 353       eapply transitivity; [ idtac | apply left_identity ].
 354       eapply comp_respects; [ idtac | reflexivity ].
 355       eapply transitivity.
 356         eapply comp_respects; [ idtac | reflexivity ].
 357         eapply symmetry.
 358         apply (mf_consistent(PreMonoidalFunctor:=CM)).
 359         apply iso_comp1.
 360
 361     eapply symmetry.
 362       eapply transitivity.
 363       setoid_rewrite <- fmor_preserves_comp.
 364       setoid_rewrite <- fmor_preserves_comp.
 365       eapply reflexivity.
 366       eapply symmetry.
 367
 368     apply comp_respects; try reflexivity.
 369
 370     eapply transitivity.
 371       apply associativity.
 372       eapply transitivity.
 373       apply associativity.
 374       eapply transitivity.
 375       apply associativity.
 376       eapply transitivity.
 377       apply associativity.
 378       apply comp_respects; try reflexivity.
 379
 380     eapply transitivity.
 381       eapply comp_respects; [ reflexivity | idtac ].
 382       eapply transitivity.
 383       eapply comp_respects; [ idtac | reflexivity ].
 384       apply mf_consistent.
 385       eapply transitivity.
 386       eapply comp_respects; [ reflexivity | idtac ].
 387         apply associativity.
 388       apply iso_comp1_right.
 389
 390     eapply transitivity.
 391       eapply comp_respects; [ reflexivity | idtac ].
 392       eapply transitivity.
 393         apply associativity.
 394       eapply comp_respects; [ reflexivity | idtac ].
 395       eapply transitivity.
 396         eapply symmetry.
 397         apply associativity.
 398       eapply transitivity; [ idtac | apply left_identity ].
 399       eapply comp_respects; [ idtac | reflexivity ].
 400       eapply transitivity.
 401         eapply comp_respects; [ idtac | reflexivity ].
 402         eapply symmetry.
 403         eapply (mf_consistent(PreMonoidalFunctor:=reification)).
 404       apply iso_comp1.
 405
 406     eapply transitivity.
 407       eapply comp_respects; [ reflexivity | idtac ].
 408       eapply symmetry.
 409       apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 410       eapply transitivity; [ idtac | apply right_identity ].
 411
 412     eapply transitivity.
 413       eapply symmetry.
 414       apply associativity.
 415     eapply transitivity.
 416       eapply comp_respects; [ idtac | reflexivity ].
 417       unfold functor_fobj.
 418       apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 419
 420     apply symmetry.
 421       eapply transitivity.
 422       apply right_identity.
 423       apply symmetry.
 424       eapply transitivity; [ idtac | apply left_identity ].
 425       apply comp_respects; [ idtac | reflexivity ].
 426
 427     eapply transitivity.
 428       Focus 2.
 429       eapply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 430       idtac.
 431       apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) (reification_rstar_obj reification A))).
 432       apply iso_comp2.
 433     Defined.
 434
 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]].
 438
 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).
 446
 447     intros.
 448       eapply transitivity.
 449         apply associativity.
 450         eapply transitivity.
 451         apply associativity.
 452         eapply transitivity.
 453         apply associativity.
 454         apply symmetry.
 455         set (@iso_shift_right') as q.
 456         simpl in q.
 457         apply q.
 458         clear q.
 459
 460       eapply symmetry.
 461         eapply transitivity.
 462         apply comp_respects; [ reflexivity | idtac ].
 463         set (mf_assoc(PreMonoidalFunctor:=reification)) as q.
 464         eapply transitivity.
 465         eapply symmetry.
 466         apply associativity.
 467         apply q.
 468
 469       eapply transitivity.
 470         eapply symmetry.
 471         apply associativity.
 472         apply comp_respects; try reflexivity.
 473         eapply transitivity.
 474         eapply symmetry.
 475         apply associativity.
 476         eapply transitivity; [ idtac | apply left_identity ].
 477         apply comp_respects; try reflexivity.
 478
 479       eapply transitivity.
 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) _)).
 484       apply iso_comp2.
 485       Qed.
 486
 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)).
 495     intros.
 496       eapply transitivity.
 497         apply associativity.
 498         eapply transitivity.
 499         apply associativity.
 500         set (@iso_shift_right') as q.
 501         apply symmetry.
 502         simpl in q.
 503         apply q.
 504         clear q.
 505
 506       eapply symmetry.
 507         eapply transitivity.
 508         apply comp_respects; [ reflexivity | idtac ].
 509         set (mf_assoc(PreMonoidalFunctor:=CM)) as q.
 510         apply q.
 511
 512       eapply transitivity.
 513         eapply symmetry.
 514         apply associativity.
 515         apply comp_respects; try reflexivity.
 516         eapply transitivity.
 517           eapply symmetry.
 518           apply associativity.
 519         eapply transitivity; [ idtac | apply left_identity ].
 520         apply comp_respects; try reflexivity.
 521
 522       eapply transitivity.
 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) _)).
 527       apply iso_comp2.
 528       Qed.
 529
 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).
 536     Opaque Underlying.
 537     eapply transitivity.
 538       eapply transitivity; [ idtac | apply right_identity ].
 539       eapply comp_respects; [ eapply reflexivity | idtac ].
 540       reflexivity.
 541
 542     apply symmetry.
 543       eapply transitivity.
 544       eapply transitivity; [ idtac | apply left_identity ].
 545       eapply comp_respects; [ idtac | eapply reflexivity ].
 546       eapply transitivity; [ idtac | apply right_identity ].
 547       apply comp_respects.
 548       simpl.
 549       apply (fmor_preserves_id (ebc_first (garrow_functor c))).
 550       reflexivity.
 551
 552     symmetry.
 553       eapply transitivity.
 554       eapply transitivity; [ idtac | apply right_identity ].
 555       apply comp_respects.
 556       reflexivity.
 557       simpl.
 558       apply (fmor_preserves_id (ebc_second (garrow_functor a))).
 559       symmetry.
 560
 561     unfold functor_fobj.
 562       unfold garrow_functor.
 563       unfold step2_functor.
 564       Opaque R'.
 565       Opaque ff_functor_section_functor.
 566       unfold functor_comp.
 567       simpl.
 568       Transparent R'.
 569       Transparent ff_functor_section_functor.
 570       idtac.
 571       apply (me_faithful(MonicEnrichment:=CMon)).
 572       eapply transitivity; [ eapply full_roundtrip | idtac ].
 573
 574     unfold fmor at 1.
 575       unfold R'.
 576       unfold me_homfunctor.
 577       eapply transitivity.
 578         eapply comp_respects; [ idtac | apply reflexivity ].
 579         eapply comp_respects; [ apply reflexivity | idtac ].
 580         eapply symmetry.
 581         apply assoc_lemma1.
 582
 583       apply symmetry.
 584         eapply transitivity.
 585         eapply symmetry.
 586         apply assoc_lemma2.
 587
 588       simpl.
 589         eapply transitivity.
 590         eapply comp_respects; [ apply reflexivity | idtac ].
 591         eapply symmetry.
 592         eapply (mf_consistent(PreMonoidalFunctor:=CM)).
 593         apply symmetry.
 594         eapply transitivity.
 595         eapply symmetry.
 596         apply associativity.
 597         apply comp_respects; [ idtac | apply reflexivity ].
 598
 599       eapply transitivity.
 600         apply associativity.
 601         eapply transitivity.
 602         apply associativity.
 603         symmetry.
 604         eapply transitivity.
 605         apply associativity.
 606         apply comp_respects; [ reflexivity | idtac ].
 607
 608       apply symmetry.
 609         eapply transitivity.
 610         apply comp_respects; [ reflexivity | idtac ].
 611         eapply transitivity.
 612         eapply symmetry.
 613         apply associativity.
 614         eapply transitivity.
 615         apply comp_respects; [ idtac | reflexivity ].
 616         eapply transitivity.
 617         apply associativity.
 618         eapply transitivity.
 619         eapply transitivity.
 620         apply comp_respects; [ reflexivity | idtac ].
 621         apply comp_respects; [ idtac | reflexivity ].
 622         eapply symmetry.
 623         apply (mf_consistent(PreMonoidalFunctor:=reification)).
 624         apply comp_respects; [ reflexivity | idtac ].
 625         apply iso_comp1.
 626         apply right_identity.
 627         eapply transitivity.
 628         eapply symmetry.
 629         apply associativity.
 630         eapply transitivity.
 631         apply comp_respects; [ idtac | reflexivity ].
 632         eapply transitivity.
 633         apply associativity.
 634         apply comp_respects; [ reflexivity | idtac ].
 635         eapply symmetry.
 636         eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 637         eapply transitivity.
 638         eapply transitivity.
 639         apply comp_respects; [ reflexivity | idtac ].
 640         eapply transitivity.
 641           eapply symmetry.
 642           apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
 643         apply comp_respects; [ idtac | reflexivity ].
 644         eapply symmetry.
 645           apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
 646         apply comp_respects; [ reflexivity | idtac ].
 647           apply associativity.
 648         eapply transitivity.
 649           eapply symmetry.
 650           apply associativity.
 651         apply comp_respects; [ idtac | reflexivity ].
 652         eapply transitivity.
 653         eapply transitivity.
 654         apply associativity.
 655         apply comp_respects; [ reflexivity | idtac ].
 656         eapply transitivity.
 657         apply associativity.
 658         eapply transitivity; [ idtac | apply right_identity ].
 659         apply comp_respects; [ reflexivity | idtac ].
 660         eapply transitivity.
 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) _)).
 665         apply iso_comp1.
 666         apply reflexivity.
 667
 668       eapply transitivity.
 669         eapply symmetry.
 670         apply associativity.
 671         eapply transitivity.
 672         eapply symmetry.
 673         apply associativity.
 674         eapply symmetry.
 675         eapply transitivity.
 676         eapply symmetry.
 677         apply associativity.
 678         apply comp_respects; [ idtac | reflexivity ].
 679
 680       apply symmetry.
 681         eapply transitivity.
 682         apply comp_respects; [ idtac | reflexivity ].
 683         eapply transitivity.
 684         apply associativity.
 685         apply comp_respects; [ reflexivity | idtac ].
 686         eapply transitivity.
 687         eapply symmetry.
 688         apply associativity.
 689         apply comp_respects; [ idtac | reflexivity ].
 690         eapply transitivity.
 691         apply comp_respects; [ reflexivity | idtac ].
 692         apply associativity.
 693         apply iso_comp1_right.
 694
 695       eapply transitivity.
 696         apply comp_respects; [ idtac | reflexivity ].
 697         eapply transitivity.
 698         apply comp_respects; [ reflexivity | idtac ].
 699         apply associativity.
 700         eapply transitivity.
 701         eapply symmetry.
 702         apply associativity.
 703         apply comp_respects; [ idtac | reflexivity ].
 704         eapply transitivity.
 705         apply comp_respects; [ idtac | reflexivity ].
 706         eapply transitivity.
 707         apply comp_respects; [ reflexivity | idtac ].
 708         eapply transitivity.
 709         eapply symmetry.
 710         apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
 711         eapply transitivity.
 712         apply comp_respects; [ reflexivity | idtac ].
 713         eapply symmetry.
 714         apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
 715         eapply symmetry.
 716         apply associativity.
 717         eapply symmetry.
 718         apply associativity.
 719         apply reflexivity.
 720         eapply transitivity.
 721         apply comp_respects; [ idtac | reflexivity ].
 722         apply comp_respects; [ idtac | reflexivity ].
 723         eapply transitivity.
 724           apply associativity.
 725         eapply transitivity; [ idtac | apply right_identity ].
 726         apply comp_respects; [ reflexivity | idtac ].
 727         eapply transitivity.
 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) _)).
 731         eapply transitivity.
 732           apply comp_respects; [ idtac | reflexivity ].
 733           eapply mf_consistent.
 734           apply iso_comp1.
 735
 736       eapply transitivity.
 737         apply associativity.
 738         eapply transitivity.
 739         apply comp_respects; [ idtac | reflexivity ].
 740         eapply transitivity.
 741         eapply symmetry.
 742         apply associativity.
 743         apply comp_respects; [ idtac | reflexivity ].
 744         eapply symmetry.
 745         eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 746         eapply transitivity.
 747         apply associativity.
 748         eapply transitivity.
 749         apply associativity.
 750         set (fun a b => isos_forward_equal_then_backward_equal _ _ (mf_consistent(PreMonoidalFunctor:=CM) a b)) as q.
 751         apply symmetry.
 752         eapply transitivity.
 753         apply comp_respects; [ idtac | reflexivity ].
 754         set (q (garrow_fobj b) (garrow_fobj a)) as q'.
 755         simpl in q'.
 756         set (fun qq => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) qq) _ _ q') as q''.
 757         eapply symmetry.
 758         apply q''.
 759         apply comp_respects; [ reflexivity | idtac ].
 760
 761       apply symmetry.
 762         eapply transitivity.
 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.
 769         simpl 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'.
 772           eapply transitivity.
 773           apply comp_respects; [ idtac | reflexivity ].
 774           apply symmetry in yy'.
 775           eapply transitivity; [ idtac | apply yy' ].
 776           eapply symmetry.
 777           apply iso_inv_inv.
 778         clear yy' yy.
 779           apply iso_shift_right' in xx.
 780           apply symmetry in xx.
 781           idtac.
 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)
 784          ~~
 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.
 788           eapply transitivity.
 789           apply associativity.
 790           apply xx.
 791           apply H.
 792           clear q.
 793         eapply transitivity.
 794           apply comp_respects; [ reflexivity | idtac ].
 795           eapply transitivity.
 796           apply comp_respects; [ idtac | reflexivity ].
 797           eapply symmetry.
 798           apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_mon C) _)).
 799           eapply transitivity.
 800           apply associativity.
 801           apply comp_respects; [ reflexivity | idtac ].
 802           eapply transitivity.
 803           eapply symmetry.
 804           apply associativity.
 805           apply comp_respects; [ idtac | reflexivity ].
 806           eapply transitivity.
 807           eapply symmetry.
 808           apply associativity.
 809           eapply transitivity; [ idtac | apply left_identity ].
 810           apply comp_respects; [ idtac | reflexivity ].
 811           eapply transitivity.
 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) _)).
 816           eapply transitivity.
 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) _)).
 821           apply iso_comp2.
 822
 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.
 826         eapply transitivity.
 827         apply comp_respects; [ reflexivity | idtac ].
 828         eapply transitivity.
 829         eapply symmetry.
 830         eapply associativity.
 831         apply comp_respects; [ idtac | reflexivity ].
 832         eapply transitivity.
 833         apply comp_respects; [ reflexivity | idtac ].
 834         eapply transitivity.
 835           eapply isos_forward_equal_then_backward_equal.
 836           apply (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C)).
 837           apply iso_inv_inv.
 838           eapply symmetry.
 839           eapply xx.
 840           clear xx.
 841         eapply transitivity.
 842           apply comp_respects; [ reflexivity | idtac ].
 843           eapply transitivity.
 844           eapply associativity.
 845           apply comp_respects; [ reflexivity | idtac ].
 846           eapply transitivity.
 847           apply comp_respects; [ reflexivity | idtac ].
 848           eapply symmetry.
 849           apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
 850           eapply transitivity.
 851           eapply symmetry.
 852           eapply associativity.
 853           eapply transitivity; [ idtac | apply left_identity ].
 854           apply comp_respects; [ idtac | reflexivity ].
 855           eapply transitivity.
 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) _)) ].
 859             apply fmor_respects.
 860           eapply transitivity.
 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) _)).
 865           apply iso_comp2.
 866
 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.
 869         simpl in xx.
 870         eapply transitivity.
 871         apply comp_respects; [ reflexivity | idtac ].
 872         eapply transitivity.
 873           apply comp_respects; [ idtac | reflexivity ].
 874           eapply symmetry.
 875           apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
 876           apply xx.
 877         eapply transitivity.
 878           eapply symmetry.
 879           apply associativity.
 880         apply symmetry.
 881           eapply transitivity.
 882           eapply symmetry.
 883           apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
 884         apply symmetry.
 885         eapply transitivity; [ idtac | apply left_identity ].
 886           apply comp_respects; [ idtac | reflexivity ].
 887         eapply transitivity.
 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) _)) ].
 891           apply fmor_respects.
 892           apply iso_comp2.
 893       Qed.
 894
 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.
 901     unfold Proper in 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'.
 905     clear q qq.
 906     setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
 907     eapply transitivity; [ apply q' | idtac ].
 908     clear q'.
 909     setoid_rewrite <- associativity.
 910     apply comp_respects; try reflexivity.
 911     symmetry.
 912     apply iso_shift_left.
 913     setoid_rewrite iso_comp1.
 914     symmetry.
 915     eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
 916     apply (fmor_respects (-⋉ F b)).
 917     apply iso_comp2.
 918     Qed.
 919
 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).
 924     Opaque Underlying.
 925     Opaque fmor.
 926     intros; simpl.
 927       setoid_rewrite right_identity.
 928       symmetry.
 929       eapply transitivity; [ idtac | apply left_identity ].
 930       apply comp_respects.
 931       apply (fmor_preserves_id (ebc_first (garrow_functor b))).
 932       unfold garrow_functor.
 933       unfold step2_functor.
 934       Transparent fmor.
 935       unfold functor_fobj.
 936       unfold functor_comp.
 937       simpl.
 938
 939       apply (me_faithful(MonicEnrichment:=CMon)).
 940       eapply transitivity; [ eapply full_roundtrip | idtac ].
 941
 942       eapply transitivity.
 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 ].
 948       eapply symmetry.
 949       apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
 950
 951       apply symmetry.
 952       apply iso_shift_left.
 953
 954       symmetry.
 955       eapply transitivity.
 956       eapply transitivity.
 957       apply associativity.
 958       apply comp_respects; [ reflexivity | idtac ].
 959       eapply transitivity.
 960       apply associativity.
 961       eapply transitivity.
 962       apply associativity.
 963       apply comp_respects; [ reflexivity | idtac ].
 964       eapply transitivity.
 965       apply associativity.
 966       apply comp_respects; [ reflexivity | idtac ].
 967       eapply symmetry.
 968       set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
 969       eapply transitivity; [ idtac | apply associativity ].
 970       apply q.
 971
 972       apply iso_shift_left'.
 973       eapply transitivity.
 974       apply associativity.
 975       symmetry.
 976       set (@iso_shift_right') as qq.
 977       simpl in qq.
 978       apply qq.
 979       clear qq.
 980       unfold me_homfunctor.
 981       eapply transitivity.
 982       symmetry.
 983       apply (cancell_lemma CM (garrow_fobj b)).
 984
 985       apply symmetry.
 986       eapply transitivity.
 987       apply comp_respects; [ idtac | reflexivity ].
 988       eapply transitivity.
 989       eapply symmetry.
 990       eapply associativity.
 991       apply comp_respects; [ idtac | reflexivity ].
 992       eapply symmetry.
 993       eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
 994
 995       eapply transitivity.
 996       apply associativity.
 997       eapply transitivity.
 998       apply associativity.
 999       apply comp_respects; try reflexivity.
1000
1001       unfold functor_fobj.
1002       unfold pmon_I.
1003
1004       set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
1005       eapply transitivity.
1006       eapply symmetry.
1007       apply associativity.
1008       eapply transitivity.
1009       apply comp_respects; [ idtac | reflexivity ].
1010       eapply symmetry.
1011       apply q.
1012       clear q.
1013       unfold fmor; simpl.
1014
1015       eapply transitivity.
1016       apply associativity.
1017       eapply transitivity; [ idtac | apply right_identity ].
1018       apply comp_respects; try reflexivity.
1019       apply iso_comp2.
1020       Qed.
1021
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'.
1032     clear q qq.
1033     setoid_rewrite (fmor_preserves_comp (F b ⋊ -)) in q'.
1034     eapply transitivity; [ apply q' | idtac ].
1035     clear q'.
1036     setoid_rewrite <- associativity.
1037     apply comp_respects; try reflexivity.
1038     symmetry.
1039     apply iso_shift_left.
1040     eapply transitivity.
1041       apply comp_respects; [ idtac | reflexivity ].
1042       apply mf_consistent.
1043     setoid_rewrite iso_comp1.
1044     symmetry.
1045     eapply transitivity; [ idtac | eapply (fmor_preserves_id (F b ⋊ - ))].
1046     apply (fmor_respects (F b ⋊ -)).
1047     apply iso_comp2.
1048     Qed.
1049
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).
1054     Opaque Underlying.
1055     Opaque fmor.
1056     intros; simpl.
1057       setoid_rewrite right_identity.
1058       symmetry.
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.
1064       Transparent fmor.
1065       unfold functor_fobj.
1066       unfold functor_comp.
1067       simpl.
1068
1069       apply (me_faithful(MonicEnrichment:=CMon)).
1070       eapply transitivity; [ eapply full_roundtrip | idtac ].
1071
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 ].
1078       eapply symmetry.
1079       apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
1080
1081       apply symmetry.
1082       apply iso_shift_left.
1083
1084       symmetry.
1085       eapply transitivity.
1086       eapply transitivity.
1087       apply associativity.
1088       apply comp_respects; [ reflexivity | idtac ].
1089       eapply transitivity.
1090       apply associativity.
1091
1092       set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
1093       setoid_rewrite associativity in q.
1094
1095       eapply transitivity.
1096       apply associativity.
1097       eapply transitivity.
1098       apply associativity.
1099       apply comp_respects; [ reflexivity | idtac ].
1100       eapply transitivity.
1101       eapply symmetry.
1102       apply associativity.
1103       eapply transitivity.
1104       apply comp_respects; [ idtac | reflexivity ].
1105       symmetry.
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.
1114       eapply symmetry.
1115       apply q.
1116
1117       apply iso_shift_left'.
1118       eapply transitivity.
1119       apply associativity.
1120       symmetry.
1121       set (@iso_shift_right') as qq.
1122       simpl in qq.
1123       apply qq.
1124       clear qq.
1125       unfold me_homfunctor.
1126       eapply transitivity.
1127       symmetry.
1128       apply (cancelr_lemma CM (garrow_fobj b)).
1129
1130       unfold functor_fobj.
1131       unfold pmon_I.
1132
1133       set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
1134       apply symmetry.
1135       eapply transitivity.
1136       apply comp_respects; [ idtac | reflexivity ].
1137       apply comp_respects; [ reflexivity | idtac ].
1138       eapply symmetry.
1139       apply q.
1140       clear q.
1141
1142       eapply transitivity.
1143       apply associativity.
1144       apply comp_respects; try reflexivity.
1145       simpl.
1146
1147       eapply transitivity.
1148       apply associativity.
1149       eapply transitivity; [ idtac | apply right_identity ].
1150       apply comp_respects; try reflexivity.
1151       apply iso_comp2.
1152       Qed.
1153
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.
1163     Defined.
1164
1165   Definition garrow_from_reification : GeneralizedArrow K C :=
1166     {| ga_functor_monoidal := garrow_monoidal
1167      ; ga_host_lang_pure   := reification_host_lang_pure _ _ _ reification
1168     |}.
1169
1170 End GArrowFromReification.
1171