: reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
simpl.
unfold mon_f.
unfold garrow_functor.
apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
: reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
simpl.
unfold mon_f.
unfold garrow_functor.
apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).