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


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.