Commit 2020-04-04 05:20 906874e2

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.