+ (* The poorly-named "step1_functor" is a functor from the full subcategory in the range of the reification functor
+ * to the full subcategory in the range of the [host language's] Hom(I,-) functor *)
+ Definition step1_functor : Functor (enr_v_mon K) (FullImage (HomFunctor C (me_i C))) garrow_fobj'.