Def CategoryTheory.Limits.Functor.isInitialConst

Modification history

2026-08-17 12:02
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
chore(CategoryTheory/Limits/Shapes/Terminal): use `to_dual` (#42842) …
Deleted CategoryTheory.Limits.Functor.isInitialConstView on Github →
2026-03-20 18:13
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types (#35867) …
Added CategoryTheory.Limits.Functor.isInitialConstView on Github →