Commit 2019-01-23 13:24 c06fb67c
View on Github →refactor(category_theory/category): split off has_hom This gives a little more flexibility when defining a category, which will be used for opposite categories. It should also be useful for defining the free category on a graph.