Concrete Category

A concrete category is a category $\mathcal{C}$ along with a Faithful Functor $U:\mathcal{C}\to\mathrm{Sets}{.}$ into the Category of Sets.

More generally, a concrete category is a Displayed Category $\mathcal{E}\rightarrowtriangle\mathcal{B}$ where every displayed hom set is an H-Proposition.