Are there diagonal functors in mathlib?

Stream: Is there code for X?

[Fernando Chu]

I mean the diagonal functors $\Delta : X \to X^C$, as well as their relation with (co)limits. If not, where should I add them?

[Adam Topaz]

We have this. Let me find it for you

[Junyan Xu]

docs#CategoryTheory.Functor.const, used in the definition of docs#CategoryTheory.Functor.cones

[Junyan Xu]

Actually, it's used in the definition of docs#CategoryTheory.Limits.Cone as well, and we have docs#CategoryTheory.Limits.Cone.isLimitEquivIsTerminal. Though we much more often work with docs#CategoryTheory.Limits.IsLimit.

[Fernando Chu]

Thanks!