A more interesting example: substitute natural numbers with binary trees. After all, they're equivalent. Now univalence would have to implement the binary tree

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.