# How do you formally check if one type is polymorphically substitutable for another type?

I want a notation that is a predicate "$$C$$ is a concrete category", and for that I need to somehow check that $$\text{Ob}$$ of $$C$$ returns a set, right?

If so, then what is the type theoretical way of stating that?

Because if my objects are sets, then we're allowed to "take an element". I am coding on the engine and specification language for doing that (a visual diagramming tool).