Commit 2025-05-24 09:54 fe6ff4a5

View on Github →

feat(CategoryTheory): IsDiscrete implies IsGroupoid (#25136) Show the Prop-class version of the fact that any discrete categories is a groupoid.

Estimated changes