Oh, well then could you point me to a formal definition of the syntax and semantics for the unary "..." operator then? What is then domain and codomain, for example?

Much obliged.