0
$\begingroup$

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).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.