# A formal definition of forgetful functor

I have read in many category theory textbooks the term "forgetful functor". But no has ever given me a precise definition of this term. I want a rigorous definition, not merely an answer that basically says, "I know it when I see it.". Has someone developed a perfectly rigorous definition of forgetful functors? This question is different from the duplicate because even there the answer was basically, "I know it when I see it".

Too narrow: Consider, for example, the functor $\text{Set} \times \text{Set} \to \text{Set}$ given by the projection to the first coordinate. I would argue that this functor deserves to be called "forgetful," since what you are forgetting is the second set (in the nLab's terminology, this functor "forgets stuff"). But it clearly isn't faithful!
Too broad: Probably a simpler example is possible, but consider the following. There is a functor $L \mapsto U(L)$ from Lie algebras to Hopf algebras given by taking the universal enveloping algebra. At least over a field of characteristic $0$, this functor is not only faithful, it is fully faithful. But I would argue that it does not deserve to be called a forgetful functor, because it was not defined by "forgetting" anything about Lie algebras. If you ever write somewhere the phrase "the forgetful functor from Lie algebras to Hopf algebras," you'll confuse people.