Objects of a category up to an isomorphism #
is_isomorphic X Y := nonempty (X ≅ Y) is an equivalence relation on the objects of a category.
The quotient with respect to this relation defines a functor from our category to
X is isomorphic to an object
X ≅ Y is not empty.
is_isomorphic defines a setoid.
The functor that sends each category to the quotient space of its objects up to an isomorphism.