Def CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit

Modification history

2026-03-20 18:13
Mathlib/CategoryTheory/Limits/Types/Products.lean
feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types (#35867) …
Added CategoryTheory.Limits.Types.isTerminalEquivIsoPUnitView on Github →