[mmhsieh]

I thought it worked. It was his way of demonstrating one of his own requirements:

(Preservation of quality, I) Every "natural" concept in 𝑋 X should be easily expressible using the notation.

So, if he is going to commit to his idea of the notation-to concept-isomorphism, it would have been weirder if he did NOT introduce the notion of the inverse map.