Theorem CategoryTheory.NatTrans.naturality_apply

Modification history

2025-02-25 18:31
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
refactor(CategoryTheory/ConcreteCategory): concreteify `NatTrans.naturality_apply` (#22275) …
Modified CategoryTheory.NatTrans.naturality_applyView on Github →
2025-01-17 14:00
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) …
Modified CategoryTheory.NatTrans.naturality_applyView on Github →
2024-05-28 19:29
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
feat: morphisms of presheaves that are locally injective for a Grothendieck topology (#11719) …
Added CategoryTheory.NatTrans.naturality_applyView on Github →