I like your explanation overall. But "point-to-point equivalence" is a little off from the math notion of homomorphism, and I think also the type theory version, if I understand correctly how you're using that phrase. It seems to imply that the homomorphism is 1-to-1 (as does the phrase "if you know the mapping you can turn one into the other"), which isn't necessarily required for the mathematical idea of a homomorphism: homomorphisms can map multiple elements of the source space to a single element of the destination space. So there may not be a well-defined way to 'go back' from the result of applying the homomorphism to the original input. (A homomorphism that isn't 'lossy' in this way is called an isomorphism.)

An example is reduction mod 5: it's a (ring) homomorphism because the relevant laws of arithmetic work just the same if you do arithmetic in the ordinary integers then reduce the result mod 5, or if you instead reduce all numbers mod 5 first and then apply special 'modulo 5' versions of those arithmetic operations. (E.g. 7 + 19 = 26 = 1 mod 5, but also (7 mod 5 + 19 mod 5) = (2 mod 5) + (4 mod 5) = 1 mod 5, where that last '+' is addition mod 5 instead of integer addition.) But you don't, given just '1 mod 5', know whether the original source integer was 1, 6, 21, -4, or any of infinitely many other choices.

Another example: projecting 3d space down to 2d by just dropping the third coordinate: (x, y, z) -> (x, y). That's a vector space homomorphism, but there isn't a way to recover the z-coordinate given just (x, y).

An example from the Haskell wiki mentioned above (I think you're referring to https://en.wikibooks.org/wiki/Haskell/Monoids#Homomorphisms) is the `length` function: given only the result of applying the homomorphism, `length(a)`, it's not possible to recover a.