Commit 2020-10-05 05:24 9ab7f055

View on Github →

feat(category_theory/limits/terminal): limit of a diagram with initial object (#4404) If the index category for a functor has an initial object, the image of the functor is a limit.

Estimated changes

Modified src/category_theory/limits/shapes/terminal.lean

modified def category_theory.limits.as_empty_cocone

modified def category_theory.limits.as_empty_cone

added def category_theory.limits.cocone_of_diagram_terminal

added def category_theory.limits.colimit_of_diagram_terminal

added def category_theory.limits.colimit_of_terminal

added def category_theory.limits.cone_of_diagram_initial

added def category_theory.limits.limit_of_diagram_initial

added def category_theory.limits.limit_of_initial