Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-02 21:56 36e5ff4c

View on Github →

feat(category_theory/with_term): formally adjoin terminal / initial objects. (#6966) Adds the construction which formally adjoins a terminal resp. initial object to a category.

Estimated changes