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.

def CategoryTheory.IsIsomorphic {C : Type u} [Category.{v, u} C] : C → C → Prop

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

Equations

• CategoryTheory.IsIsomorphic X Y = Nonempty (X ≅ Y)

def CategoryTheory.isIsomorphicSetoid (C : Type u) [Category.{v, u} C] : Setoid C

IsIsomorphic defines a setoid.

Equations

• CategoryTheory.isIsomorphicSetoid C = { r := CategoryTheory.IsIsomorphic, iseqv := ⋯ }

def CategoryTheory.isomorphismClasses : Functor Cat (Type u)

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.

theorem CategoryTheory.Groupoid.isIsomorphic_iff_nonempty_hom {C : Type u} [Groupoid C] {X Y : C} : IsIsomorphic X Y ↔ Nonempty (X ⟶ Y)