The author is correct that checking if two functions having infinite domains are equal is often impossible. He also has correct statements of some mathematical theorems. But people in this thread have provided counterexamples to his claim. That means he needs to fix the mistakes he made.
If you are interested in what serious mathematicians have to say on this topic see https://homotopytypetheory.org/.
It is possible in certain cases, that's the point of the article. One of the contributors to HoTT is the author of the paper introducing these algorithms :)
