Terminal object of `cone F`

Stream: Is there code for X?

[Andrew Yang]

Do we know that a cone is a limit cone iff it is terminal in the category of cone F?

[Floris van Doorn]

The closest I can find is docs#category_theory.limits.is_limit.iso_unique_cone_morphism and docs#category_theory.limits.is_terminal.of_unique

[Andrew Yang]

Thanks! Hopefully I can fit them together to get something that works cleanly.
It's probably worthy to be stated out explicitly though, but that might be too much of a detour for me.

[Scott Morrison]

That is a weird gap. :-( We certainly want to have it.

[Andrew Yang]

Turns out I couldn't get away without it. I'll make a PR for it.