category_theory.groupoid

A groupoid is a category such that all morphisms are isomorphisms.

category_theory.groupoid.iso_equiv_hom

In a groupoid, isomorphisms are equivalent to morphisms.