That theorem is not valid constructively, so no way to make a computer program out of it. I.e., there is no program that given types A, B and injections (f : A -> B) and (g : B -> A) produces a bijection A -> B.
But from reading the first bit of the paper I think they are talking about something stronger, not any bijection but one that only requires inspecting and manipulating a bounded number of layers of the trees.
