Further overhauling of (now) uu0a. Notice that the notation f ~ g
was introduced for homotopies, and consequently removed from the
K-Theory files due to conflict.