: Reification K C (mon_i C).
refine
{| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow
; reification_rstar_f := garrow >>>> me_mf C
: Reification K C (mon_i C).
refine
{| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow
; reification_rstar_f := garrow >>>> me_mf C