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.

Estimated changes