Def CategoryTheory.uniqueHomsetOfInitialIsoTerminal

Modification history

2024-11-14 20:44
Mathlib/CategoryTheory/Closed/Zero.lean
refactor: change `CartesianClosed` to rely on `ChosenFiniteProducts` (#17766) …
Deleted CategoryTheory.uniqueHomsetOfInitialIsoTerminalView on Github →
2023-06-10 00:02
Mathlib/CategoryTheory/Closed/Zero.lean
feat: port CategoryTheory.Closed.Zero (#4921)
Added CategoryTheory.uniqueHomsetOfInitialIsoTerminalView on Github →