feat(category_theory): quotient categories (#2310)
This constructs the quotient of a category by an arbitrary family of relations on its hom-sets. Analogous to "quotient of a group by the normal closure of a subset", as opposed to "quotient of a group by a normal subgroup".
The plan is to eventually use this together with the path category to construct the free groupoid on a graph.
