Commit 2025-03-29 21:33 40f3d5c3
View on Github →feat(CategoryTheory/Groupoid): IsGroupoid typeclass (#23307)
Add a IsGroupoid typeclass that asserts that a category is a groupoid, i.e that every morphism is an isomorphism. Add the IsGroupoid pendent of some of the instances in CategoryTheory.Groupoid.