Theorem CategoryTheory.NatTrans.naturality_apply

Modification history

2026-02-06 21:24
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
refactor(CategoryTheory): remove `HasForget` (#34741)
Modified CategoryTheory.NatTrans.naturality_applyView on Github →
2025-12-13 14:21
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.NatTrans.naturality_applyView on Github →
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 →