CatGloss

A concrete category is a category $\mathsf{C}$ equipped with a faithful functor $U \colon \mathsf{C} \to \textup{\textsf{cat}}$.