| 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$
Wikipedia: Faithful functor