+Implicit Arguments mf_first [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+Implicit Arguments mf_second [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+Implicit Arguments mf_i [[Ob] [Hom] [C1] [bin_obj'] [bc] [I1] [PM1] [Ob0] [Hom0] [C2] [bin_obj'0] [bc0] [I2] [PM2] [fobj] [F]].
+
+ Lemma assoc_lemma1 : forall a b c,
+ iso_backward ((mf_first reification c) (a ⊗ b)) >>>
+ iso_backward ((mf_second reification a) b) ⋉ reification c >>>
+ #(pmon_assoc(PreMonoidalCat:=enr_v_mon C) (reification a) (reification c) (reification_rstar_obj reification b)) >>>
+ reification a ⋊ #((mf_first reification c) b) >>>
+ #((mf_second reification a) (b ⊗ c)) ~~
+ reification \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
+
+ intros.
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply symmetry.
+ set (@iso_shift_right') as q.
+ simpl in q.
+ apply q.
+ clear q.
+
+ eapply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ set (mf_assoc(PreMonoidalFunctor:=reification)) as q.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply q.
+
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects; try reflexivity.
+
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ apply iso_comp2.
+ Qed.
+
+ Lemma assoc_lemma2 : forall a b c,
+ iso_backward ((mf_first CM (garrow_fobj c)) _) >>>
+ (bin_first(BinoidalCat:=enr_v_bin C) _ \ iso_backward ((mf_second CM (garrow_fobj a)) (garrow_fobj b))) >>>
+ (#((pmon_assoc(PreMonoidalCat:=enr_v_mon C) _ _) _) >>>
+ (bin_second(BinoidalCat:=enr_v_bin C) _ \
+ #((mf_first CM (garrow_fobj c)) (garrow_fobj b)))) >>>
+ #((mf_second CM (garrow_fobj a)) _) ~~
+ HomFunctor C _ \ #((pmon_assoc(PreMonoidalCat:=enr_c_pm C) (garrow_fobj a) (garrow_fobj c)) (garrow_fobj b)).
+ intros.
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ set (@iso_shift_right') as q.
+ apply symmetry.
+ simpl in q.
+ apply q.
+ clear q.
+
+ eapply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ set (mf_assoc(PreMonoidalFunctor:=CM)) as q.
+ apply q.
+
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects; try reflexivity.
+
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ apply iso_comp2.
+ Qed.
+
+ Lemma assoc_coherent (a b c : enr_v K) :
+ (#((pmon_assoc(PreMonoidalCat:=enr_c_pm C)
+ (garrow_functor a) (garrow_functor c)) (garrow_fobj b)) >>> garrow_functor a ⋊ #((garrow_first c) b)) >>>
+ #((garrow_second a) (b ⊗ c)) ~~
+ (#((garrow_second a) b) ⋉ garrow_functor c >>>
+ #((garrow_first c) (a ⊗ b))) >>> garrow_functor \ #((pmon_assoc(PreMonoidalCat:=enr_v_mon K) a c) b).
+ Opaque Underlying.
+ eapply transitivity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ eapply comp_respects; [ eapply reflexivity | idtac ].
+ reflexivity.
+
+ apply symmetry.
+ eapply transitivity.
+ eapply transitivity; [ idtac | apply left_identity ].
+ eapply comp_respects; [ idtac | eapply reflexivity ].
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects.
+ simpl.
+ apply (fmor_preserves_id (ebc_first (garrow_functor c))).
+ reflexivity.
+
+ symmetry.
+ eapply transitivity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects.
+ reflexivity.
+ simpl.
+ apply (fmor_preserves_id (ebc_second (garrow_functor a))).
+ symmetry.
+
+ unfold functor_fobj.
+ unfold garrow_functor.
+ unfold step2_functor.
+ Opaque R'.
+ Opaque ff_functor_section_functor.
+ unfold functor_comp.
+ simpl.
+ Transparent R'.
+ Transparent ff_functor_section_functor.
+ idtac.
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+ unfold fmor at 1.
+ unfold R'.
+ unfold me_homfunctor.
+ eapply transitivity.
+ eapply comp_respects; [ idtac | apply reflexivity ].
+ eapply comp_respects; [ apply reflexivity | idtac ].
+ eapply symmetry.
+ apply assoc_lemma1.
+
+ apply symmetry.
+ eapply transitivity.
+ eapply symmetry.
+ apply assoc_lemma2.
+
+ simpl.
+ eapply transitivity.
+ eapply comp_respects; [ apply reflexivity | idtac ].
+ eapply symmetry.
+ eapply (mf_consistent(PreMonoidalFunctor:=CM)).
+ apply symmetry.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | apply reflexivity ].
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ symmetry.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (mf_consistent(PreMonoidalFunctor:=reification)).
+ apply comp_respects; [ reflexivity | idtac ].
+ apply iso_comp1.
+ apply right_identity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+ apply comp_respects; [ reflexivity | idtac ].
+ apply associativity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_mon C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_mon C) _)) ].
+ apply (fmor_respects (bin_second(BinoidalCat:=enr_v_mon C) _)).
+ apply iso_comp1.
+ apply reflexivity.
+
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply symmetry.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply associativity.
+ apply iso_comp1_right.
+
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply associativity.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply symmetry.
+ apply associativity.
+ eapply symmetry.
+ apply associativity.
+ apply reflexivity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac | apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_mon C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply mf_consistent.
+ apply iso_comp1.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ set (fun a b => isos_forward_equal_then_backward_equal _ _ (mf_consistent(PreMonoidalFunctor:=CM) a b)) as q.
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ set (q (garrow_fobj b) (garrow_fobj a)) as q'.
+ simpl in q'.
+ set (fun qq => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) qq) _ _ q') as q''.
+ eapply symmetry.
+ apply q''.
+ apply comp_respects; [ reflexivity | idtac ].
+
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ set (ni_commutes (pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c))
+ #(homset_tensor_iso a)) as xx.
+ unfold functor_comp in xx.
+ simpl in xx.
+ set (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C) (reification a) (reification b) (reification c)) as yy.
+ set (isos_forward_equal_then_backward_equal _ _ yy) as yy'.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply symmetry in yy'.
+ eapply transitivity; [ idtac | apply yy' ].
+ eapply symmetry.
+ apply iso_inv_inv.
+ clear yy' yy.
+ apply iso_shift_right' in xx.
+ apply symmetry in xx.
+ idtac.
+ assert (#((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) (reification a)) ⁻¹ >>>
+ #(homset_tensor_iso a) ⋉ (reification b ⊗ reification c)
+ ~~
+ (#(homset_tensor_iso a) ⋉ reification b) ⋉ reification c >>>
+ #((pmon_assoc_rr(PreMonoidalCat:=enr_v_mon C) (reification b) (reification c)) _)⁻¹).
+ apply iso_shift_left.
+ eapply transitivity.
+ apply associativity.
+ apply xx.
+ apply H.
+ clear q.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ apply iso_comp2.
+
+ set (fun a' => ni_commutes (pmon_assoc(PreMonoidalCat:=enr_v_mon C) a' (reification c))
+ (iso_backward (homset_tensor_iso b))) as xx.
+ unfold fmor in xx; unfold functor_comp in xx; simpl in xx.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ eapply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply isos_forward_equal_then_backward_equal.
+ apply (pmon_coherent_r(PreMonoidalCat:=enr_v_mon C)).
+ apply iso_inv_inv.
+ eapply symmetry.
+ eapply xx.
+ clear xx.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity.
+ eapply symmetry.
+ eapply associativity.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
+ apply fmor_respects.
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_first(BinoidalCat:=enr_v_bin C) _)) ].
+ apply (fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) _)).
+ apply iso_comp2.
+
+ set (fun a b => ni_commutes (pmon_assoc_ll(PreMonoidalCat:=enr_v_mon C) a b)) as xx.
+ unfold functor_comp in xx.
+ simpl in xx.
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
+ apply xx.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply symmetry.
+ eapply transitivity.
+ eapply symmetry.
+ apply (pmon_coherent_l(PreMonoidalCat:=enr_v_mon C)).
+ apply symmetry.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+ eapply transitivity; [ idtac |
+ apply (fmor_preserves_id (bin_second(BinoidalCat:=enr_v_bin C) _)) ].
+ apply fmor_respects.
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancell_lemma `(F:PreMonoidalFunctor) b :
+ iso_backward (mf_i F) ⋉ (F b) >>> #(pmon_cancell (F b)) ~~
+ #((mf_first F b) _) >>> F \ #(pmon_cancell b).
+ set (mf_cancell(PreMonoidalFunctor:=F) b) as q.
+ setoid_rewrite associativity in q.
+ set (@comp_respects) as qq.
+ unfold Proper in qq.
+ unfold respectful in qq.
+ set (qq _ _ _ _ _ _ (iso_backward (mf_i F) ⋉ F b) (iso_backward (mf_i F) ⋉ F b) (reflexivity _) _ _ q) as q'.
+ setoid_rewrite <- associativity in q'.
+ clear q qq.
+ setoid_rewrite (fmor_preserves_comp (-⋉ F b)) in q'.
+ eapply transitivity; [ apply q' | idtac ].
+ clear q'.
+ setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ symmetry.
+ apply iso_shift_left.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ eapply transitivity; [ idtac | eapply (fmor_preserves_id (-⋉ F b))].
+ apply (fmor_respects (-⋉ F b)).
+ apply iso_comp2.
+ Qed.
+*)
+ Lemma cancell_coherent (b:enr_v K) :
+ #(pmon_cancell(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
+ (#(iso_id (enr_c_i C)) ⋉ garrow_functor b >>>
+ #((garrow_first b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancell(PreMonoidalCat:=enr_v_mon K) b).
+ Opaque Underlying.
+ Opaque fmor.
+ intros; simpl.
+ setoid_rewrite right_identity.
+ symmetry.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects.
+ apply (fmor_preserves_id (ebc_first (garrow_functor b))).
+ unfold garrow_functor.
+ unfold step2_functor.
+ Transparent fmor.
+ unfold functor_fobj.
+ unfold functor_comp.
+ simpl.
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_first(BinoidalCat:=enr_v_bin C) (reification b))).
+
+ apply symmetry.
+ apply iso_shift_left.
+
+ symmetry.
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ set (mf_cancell(PreMonoidalFunctor:=reification) b) as q.
+ eapply transitivity; [ idtac | apply associativity ].
+ apply q.
+
+ apply iso_shift_left'.
+ eapply transitivity.
+ apply associativity.
+ symmetry.
+ set (@iso_shift_right') as qq.
+ simpl in qq.
+ apply qq.
+ clear qq.
+ unfold me_homfunctor.
+ eapply transitivity.
+ symmetry.
+ apply (cancell_lemma CM (garrow_fobj b)).
+
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply symmetry.
+ eapply associativity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+
+ unfold functor_fobj.
+ unfold pmon_I.
+
+ set (ni_commutes (pmon_cancell(PreMonoidalCat:=enr_v_mon C))) as q.
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply q.
+ clear q.
+ unfold fmor; simpl.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; try reflexivity.
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancelr_lemma `(F:PreMonoidalFunctor) b :
+ (F b) ⋊ iso_backward (mf_i F)>>> #(pmon_cancelr (F b)) ~~
+ #((mf_first F _) _) >>> F \ #(pmon_cancelr b).
+ set (mf_cancelr(PreMonoidalFunctor:=F) b) as q.
+ setoid_rewrite associativity in q.
+ set (@comp_respects) as qq.
+ unfold Proper in qq.
+ unfold respectful in qq.
+ set (qq _ _ _ _ _ _ (F b ⋊ iso_backward (mf_i F)) (F b ⋊ iso_backward (mf_i F)) (reflexivity _) _ _ q) as q'.
+ setoid_rewrite <- associativity in q'.
+ clear q qq.
+ setoid_rewrite (fmor_preserves_comp (F b ⋊ -)) in q'.
+ eapply transitivity; [ apply q' | idtac ].
+ clear q'.
+ setoid_rewrite <- associativity.
+ apply comp_respects; try reflexivity.
+ symmetry.
+ apply iso_shift_left.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply mf_consistent.
+ setoid_rewrite iso_comp1.
+ symmetry.
+ eapply transitivity; [ idtac | eapply (fmor_preserves_id (F b ⋊ - ))].
+ apply (fmor_respects (F b ⋊ -)).
+ apply iso_comp2.
+ Qed.
+
+ Lemma cancelr_coherent (b:enr_v K) :
+ #(pmon_cancelr(PreMonoidalCat:=enr_c_pm C) (garrow_functor b)) ~~
+ (garrow_functor b ⋊ #(iso_id (enr_c_i C)) >>>
+ #((garrow_second b) (enr_v_i K))) >>> garrow_functor \ #(pmon_cancelr(PreMonoidalCat:=enr_v_mon K) b).
+ Opaque Underlying.
+ Opaque fmor.
+ intros; simpl.
+ setoid_rewrite right_identity.
+ symmetry.
+ eapply transitivity; [ idtac | apply left_identity ].
+ apply comp_respects.
+ apply (fmor_preserves_id (ebc_second (garrow_functor b))).
+ unfold garrow_functor.
+ unfold step2_functor.
+ Transparent fmor.
+ unfold functor_fobj.
+ unfold functor_comp.
+ simpl.
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ eapply transitivity; [ eapply full_roundtrip | idtac ].
+
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (fmor_preserves_comp (bin_second(BinoidalCat:=enr_v_bin C) _)).
+
+ apply symmetry.
+ apply iso_shift_left.
+
+ symmetry.
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+
+ set (mf_cancelr(PreMonoidalFunctor:=reification) b) as q.
+ setoid_rewrite associativity in q.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ symmetry.
+ eapply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply comp_respects; [ reflexivity | idtac ].
+ apply comp_respects; [ idtac | reflexivity ].
+ apply mf_consistent.
+ eapply symmetry.
+ apply q.
+
+ apply iso_shift_left'.
+ eapply transitivity.
+ apply associativity.
+ symmetry.
+ set (@iso_shift_right') as qq.
+ simpl in qq.
+ apply qq.
+ clear qq.
+ unfold me_homfunctor.
+ eapply transitivity.
+ symmetry.
+ apply (cancelr_lemma CM (garrow_fobj b)).
+
+ unfold functor_fobj.
+ unfold pmon_I.
+
+ set (ni_commutes (pmon_cancelr(PreMonoidalCat:=enr_v_mon C))) as q.
+ apply symmetry.
+ eapply transitivity.
+ apply comp_respects; [ idtac | reflexivity ].
+ apply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply q.
+ clear q.
+
+ eapply transitivity.
+ apply associativity.
+ apply comp_respects; try reflexivity.
+ simpl.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ apply comp_respects; try reflexivity.
+ apply iso_comp2.
+ Qed.
+
+ Instance garrow_monoidal : PreMonoidalFunctor (enr_v_pmon K) (enr_c_pm C) garrow_functor :=
+ { mf_first := garrow_first
+ ; mf_second := garrow_second
+ ; mf_i := iso_id _ }.
+ intros; reflexivity.
+ intros; apply (reification_host_lang_pure _ _ _ reification).
+ apply cancell_coherent.
+ apply cancelr_coherent.
+ apply assoc_coherent.