Commit 2024-10-15 13:30 33e2fef6

View on Github →

chore(CategoryTheory): Unique->Nonempty+Subsingleton (#17748) Assume [Nonempty _] [Subsingleton _] instead of [Unique _] whenever default isn't used outside of proofs.

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

modified def CategoryTheory.Limits.biproductUniqueIso

modified def CategoryTheory.Limits.limitBiconeOfUnique

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

modified def CategoryTheory.Limits.colimitCoconeOfUnique

modified def CategoryTheory.Limits.coproductUniqueIso

modified def CategoryTheory.Limits.limitConeOfUnique

modified def CategoryTheory.Limits.productUniqueIso

Modified Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

modified theorem CategoryTheory.Limits.hasInitial_of_unique

modified theorem CategoryTheory.Limits.hasTerminal_of_unique