Why are limits in category noncomputable?

Stream: mathlib4

[Kenny Lau]

Was this to prevent diamonds?

[Kevin Buzzard]

Because you can't compute them in general?

[Kenny Lau]

well i can just form the product type (in the category Type)

[Aaron Liu]

That a specific example of a limit which is computable

[Aaron Liu]

that doesn't mean they're computable in general

[Joël Riou]

For binary products with good definitional properties, we have the API FiniteChosenProducts.

[Adam Topaz]

And in general you can work with an explicit (co)limit (co)cone if you want to have some special properties of the (co)limit.

[Antoine Chambert-Loir]

That won't give you an algorithm to decide whether two distinct objects are some level stay distinct in every subsequent level.