[Merged by Bors] - chore(category_theory): replace has_hom with quiver

[semorrison]

---

• depends on: [Merged by Bors] - chore(combinatorics/quiver): make quiver a class #7150

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - chore(combinatorics/quiver): make quiver a class #7150

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[dwarn]

Can we split combinatorics/quiver.lean into multiple files? Otherwise, LGTM! This opens up the possibility to unify things like quiver.total / category_theory.arrow, quiver.weakly_connected_components / category_theory.connected_components, and subquivers / subcategories.

[semorrison]

Definitely. I think that's a good idea. How would you feel about doing this in a subsequent PR?

[dwarn]

Sure, I can do that.

[b-mehta]

This seems sensible to me - @semorrison are you happy to merge this?

[semorrison]

@b-mehta yes please!

[b-mehta]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests