- Definition garrow_from_reification : GeneralizedArrow K C.
- refine {| ga_functor := garrow_functor |}.
- (*
- unfold garrow_functor.
- apply MonoidalFunctorsCompose.
- apply MonoidalFunctorsCompose.
- *)
+ Lemma garrow_functor_monoidal_iso_i
+ : mon_i C ≅ garrow_functor (mon_i (enr_v_mon K)).
+ admit.
+ Defined.
+
+ Lemma garrow_functor_monoidal_iso :
+ forall X Y:enr_v_mon K,
+ garrow_functor (bin_obj(BinoidalCat:=enr_v_mon K) X Y) ≅ bin_obj(BinoidalCat:=me_mon C) (garrow_functor X) (garrow_functor Y).
+ admit.
+ Defined.
+
+ Definition garrow_functor_monoidal_niso
+ : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+ admit.
+ Defined.
+ Opaque homset_tensor_iso.
+
+ Instance garrow_functor_monoidal : MonoidalFunctor (enr_v_mon K) C garrow_functor :=
+ { mf_coherence := garrow_functor_monoidal_niso
+ ; mf_id := garrow_functor_monoidal_iso_i
+ }.