Def CategoryTheory.WithInitial.ofCommaObject

Modification history

2025-03-13 09:34

Mathlib/CategoryTheory/WithTerminal.lean

feat(CategoryTheory/WithTerminal): functors out of `WithTerminal` (#22658) …

Added CategoryTheory.WithInitial.ofCommaObject View on Github →