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.
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.