+ (* the "step2_functor" is the section of the Hom(I,-) functor *)
+ Definition step2_functor :=
+ ff_functor_section_functor _ (me_full(MonicEnrichment:=CMon)) (me_faithful(MonicEnrichment:=CMon)).
+
+ Definition garrow_functor :=
+ RestrictToImage (reification_rstar reification) >>>> (R' >>>> step2_functor).
+
+ Lemma iso_id_lemma1 `{C':Category}(a b:C')(f:a~~{C'}~~>b) : #(iso_id a) >>> f ~~ f.
+ simpl.
+ apply left_identity.
+ Qed.
+
+ Lemma iso_id_lemma2 `{C':Category}(a b:C')(f:b~~{C'}~~>a) : f >>> #(iso_id a) ~~ f.
+ simpl.
+ apply right_identity.
+ Qed.
+
+ Lemma full_roundtrip : forall a b (f:a~>b), me_homfunctor \ (ff_functor_section_fmor me_homfunctor me_full f) ~~ f.
+ intros.
+ unfold ff_functor_section_fmor.
+ set (me_full a b f) as full.
+ destruct full.
+ apply e.
+ Qed.
+
+ Opaque UnderlyingFunctor.
+ Instance garrow_first a :
+ (garrow_functor >>>> bin_first(BinoidalCat:=enr_c_bin C) (R' a)) <~~~>
+ (bin_first(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
+ { ni_iso := fun a => iso_id _ }.
+ intros.
+ etransitivity. apply iso_id_lemma1. symmetry.
+ etransitivity. apply iso_id_lemma2. symmetry.
+
+ Opaque Underlying.
+ unfold garrow_functor.
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_first (R' a)) f).
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ set (ni_commutes (mf_first(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
+ unfold functor_comp in qq.
+ simpl in qq.
+ apply iso_shift_right' in qq.
+ apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ symmetry.
+ unfold fmor at 1.
+ eapply transitivity.
+ set (ni_commutes (mf_first(PreMonoidalFunctor:=CM) (R' a))) as zz.
+ unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
+ set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
+ apply iso_shift_right' in zz'.
+ apply zz'.
+
+ unfold functor_comp; simpl.
+
+ symmetry.
+ eapply transitivity.
+ set full_roundtrip as full_roundtrip'.
+ unfold fmor in full_roundtrip'.
+ simpl in full_roundtrip'.
+ apply full_roundtrip'.
+
+ set (@iso_shift_right') as q. simpl in q. apply q. clear q.
+
+ set (@iso_shift_left) as q. simpl in q. apply q. clear q.
+
+ symmetry.
+ eapply transitivity.
+ set full_roundtrip as full_roundtrip'.
+ unfold fmor in full_roundtrip'.
+ simpl in full_roundtrip'.
+ apply (fun a' b' f z => fmor_respects (bin_first(BinoidalCat:=enr_v_bin C) z) _ _ (full_roundtrip' a' b' f)).
+ symmetry.
+
+ intros.
+ unfold bin_obj.
+ unfold senr_v_bobj.
+
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ setoid_rewrite <- associativity.
+ simpl.
+ setoid_rewrite <- associativity.
+ etransitivity.
+ apply iso_comp1_left.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ apply iso_comp1_right.
+
+ eapply symmetry.
+ eapply transitivity.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite <- fmor_preserves_comp.
+ eapply reflexivity.
+ eapply symmetry.
+
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply symmetry.
+ apply associativity.
+ apply comp_respects; try apply reflexivity.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ eapply associativity.
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ apply iso_comp1_left.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ eapply comp_respects.
+ eapply symmetry.
+ eapply associativity.
+ eapply reflexivity.
+ apply iso_comp1_left.
+
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply symmetry.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply comp_respects; [ idtac | reflexivity ].
+ eapply transitivity.
+ apply associativity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply symmetry.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=enr_v_mon C) _)).
+ eapply transitivity.
+ eapply transitivity.
+ apply associativity.
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ apply associativity.
+ eapply transitivity; [ idtac | apply right_identity ].
+ eapply comp_respects; [ reflexivity | idtac ].
+ eapply transitivity.
+ unfold functor_fobj.
+ apply fmor_preserves_comp.
+ setoid_rewrite iso_comp2.
+ apply fmor_preserves_id.
+
+ apply comp_respects.
+ reflexivity.
+ reflexivity.
+ Defined.
+
+ Instance garrow_second a :
+ (garrow_functor >>>> bin_second(BinoidalCat:=enr_c_bin C) (R' a))
+ <~~~> (bin_second(BinoidalCat:=enr_v_pmon K) a >>>> garrow_functor) :=
+ { ni_iso := fun a => iso_id _ }.
+ intros.
+ etransitivity. apply iso_id_lemma1. symmetry.
+ etransitivity. apply iso_id_lemma2. symmetry.
+
+ Opaque Underlying.
+ unfold garrow_functor.
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ apply (functor_comp_assoc (RestrictToImage reification) (R' >>>> step2_functor) (ebc_second (R' a)) f).
+ unfold functor_comp at 1.
+ unfold functor_comp at 1.
+ Opaque functor_comp. simpl. Transparent functor_comp.
+
+ symmetry.
+ eapply transitivity.
+ set (ni_commutes (mf_second(PreMonoidalFunctor:=reification_rstar reification) a) f) as qq.
+ unfold functor_comp in qq.
+ simpl in qq.
+ apply iso_shift_right' in qq.
+ apply (fmor_respects(R' >>>> step2_functor) _ _ qq).
+
+ apply (me_faithful(MonicEnrichment:=CMon)).
+ symmetry.
+ unfold fmor at 1.
+ eapply transitivity.
+ set (ni_commutes (mf_second(PreMonoidalFunctor:=CM) (R' a))) as zz.
+ unfold functor_comp in zz; unfold functor_fobj in zz; simpl in zz.
+ set (zz _ _ ((R' >>>> step2_functor) \ (reification \ f))) as zz'.
+ apply iso_shift_right' in zz'.
+ apply zz'.
+
+ unfold functor_comp; simpl.