Can noncomputationality cancel out over quotients?

Stream: new members

[Klaus Gy]

i noticed that the definition of CategoryTheory.Subobject.pullback is noncomputational because it uses CategoryTheory.MonoOver.pullback, which works by choosing pullbacks from existence. But isomorphic pullbacks give equal subobjects, so is this a limitation of Lean itself or a limitation of the implementation? In other words, could we theoretically have a computational version of CategoryTheory.Subobject.pullback (or similar patterns), where all noncomputational choices lead to the same result?

[Kenny Lau]

@Klaus Gy in Lean unique choice is still noncomputable.

[Kenny Lau]

there's no algorithm to construct the unique pullback, even if it's unique

[Kenny Lau]

it is not a "limitation" of any kind, it is just noncomputable

[Kenny Lau]

it was a choice ever since we made all limit noncomputable

[Klaus Gy]

i see, thank you!