Objects of a category up to an isomorphism #
IsIsomorphic 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.
Instances For
IsIsomorphic
defines a setoid.
Instances For
The functor that sends each category to the quotient space of its objects up to an isomorphism.
Equations
- One or more equations did not get rendered due to their size.