mathlib

5424d3f4 - feat(category_theory/limits): has_limit F ↔ has_terminal (cone F) (#15797)

feat(category_theory/limits): has_limit F ↔ has_terminal (cone F) (#15797) This will be used to show that `C` has limits of shape `J` if and only if `const J` has a right adjoint.