feat(category_theory/limits/terminal): limit of a diagram with initial object (#4404)
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.



leanprover-community/mathlib,leanprover-community/mathlib