Commit 2025-02-25 18:31 73d6d99b
View on Github →refactor(CategoryTheory/ConcreteCategory): concreteify NatTrans.naturality_apply
(#22275)
This lemma was still stated using HasForget
, we can turn it into taking ConcreteCategory
for some nice downstream cleanup.