+ 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
+ }.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+ Definition garrow_from_reification : GeneralizedArrow K C.
+ refine
+ {| ga_functor := garrow_functor
+ ; ga_functor_monoidal := garrow_functor_monoidal
+ |}.
+ Defined.
+