Commit 2026-10-01 20:57 448388c1
View on Github →fix(CategoryTheory/Monoidal/Internal/Types): remove superfluous instance (#44399) There was already an Inhabited instance in scope (Mon.instInhabited), and the inhabitants for both instances are propositionally equal, but not defeq at implicit transparency. This caused an instance diamond. Found by the linter in #38781.