mathlib3

8a032292 - feat(category_theory/limits): cone F ≌ costructured_arrow (const J) F (#15796)

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