In mathematics we often seek to classify objects up to an equivalence relation, where two objects A and B are said to be equivalent if there exists a map $f:A\rightarrow B$ satisfying certain properties. Examples include trying to classify (some class of) n-manifolds up to homeomorphism, or finite groups up to isomorphism, or (some class of) varieties modulo birational equivalence.
What examples can you give where you can prove equivalence abstractly, but there is no known algorithm to find the map which induces the equivalence?
For example, could you give examples of manifolds you could prove to be homeomorphic (or homotopic, or simple homotopic, or whatever), but where you had no algorithmic way of finding the homeomorphism between them explicitly?
I think such examples are philosophically interesting, because they highlight how much stronger weaker "proving something" might be than "calculating something", with each answer providing an example.
Inspired by this question.
