Faithful functor

definiendum	$F$ in it
inclusion	$F:{\bf C}\longrightarrow{\bf D}$
inclusion	${\bf C},{\bf D}$ … locally small
postulate	$\mathrm{fmap}(F)_{X,Y}:{\bf C}[X,Y]\to{\bf D}[FX,FY]$ … injective

Here I needed to introduc the notation $\mathrm{fmap}(F)_{X,Y}$ for the polymorphic function at $X$ and $Y$