Commit 2025-02-03 16:47 fc39d3b8
View on Github →feat(Algebra/Category): ConcreteCategory
instance for Semigrp
(#21368)
Very straightforward, essentially copypasting the design of MonCat
back onto MagmaCat
and Semigrp
. We can probably do without this amount of dsimp
lemmas, they should all be pretty easy to prove from generic ConcreteCategory
results, but it doesn't hurt to have them in any case.