Def CategoryTheory.WithInitial.mkCommaObject

Modification history

2025-03-13 09:34

Mathlib/CategoryTheory/WithTerminal.lean

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

Added CategoryTheory.WithInitial.mkCommaObject View on Github →