mathlib3 documentation


Objects of a category up to an isomorphism #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

An object X is isomorphic to an object Y, if X ≅ Y is not empty.


The functor that sends each category to the quotient space of its objects up to an isomorphism.