A more interesting example: substitute natural numbers with binary trees. After all, they're equivalent. Now univalence would have to implement the binary tree analogue for every function on naturals, in a way that preserves semantics with respect to our conversion function.

Yes, that's pretty much it. Doing this systematically for all types including dependent types that quantify over Bool, as well as for user defined higher inductive types is another matter.