Commit 2023-11-15 09:39 91e2d026

View on Github →

feat(CategoryTheory): ULift creates small (co)limits (#8209)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean

added def CategoryTheory.Limits.Types.quotEquiv

added def CategoryTheory.Limits.Types.sectionsEquiv'

added def CategoryTheory.Limits.Types.sectionsEquiv