is_limit for an object

Stream: Is there code for X?

[Chris Hughes]

Do we have a version of is_limit X for when X is an object and not a cone?

[Kevin Buzzard]

So the claim would be that there exists a cone? It would then be quite difficult to say anything about the limit object I guess because you don't have access to any of the maps!

[Chris Hughes]

I would expect is_limit X : Type

[Kevin Buzzard]

Oh, my mental naming model is is_ for Props. So it's partially bundled limits?

[Chris Hughes]

Yes

[Markus Himmel]

I don't think we have this right now. I was also thinking about this because I will need something like this soon for ind-objects and pro-objects. My plan was to just bundle together a limit cone and an isomorphism between the cone point and X.

[Adam Topaz]

A cone is "just" a morphism of functors from the constant functor associated to X. You could just write is_limit (cone.mk X e) where e is your nat. trans.

[Adam Topaz]

A while ago I suggested making something like this into a class, but @Bhavik Mehta thought it was a bad idea. I'm on mobile now, so I can't dig up that old thread. Maybe someone else can find it?

[Markus Himmel]

Ah, of course, is_limit (cone.mk X e) is a much better approach.

[Stuart Presnell]

Was that this thread?

[Adam Topaz]

Yes!