I am familiar with the notation $\exists\,!$ to express both existence and uniqueness. For example $\;\;\exists\,!x\!:\!P\,(x)\;\;$ means "there exists a unique $x$ such that $P\,(x)$ holds", for some predicate $P\,$.
Is there some similarly compact notation to denote only uniqueness (i.e. without simultaneously asserting existence)?
In other words, is there a similarly compact, "easy-to-parse" way to express the assertion "$P\,(x)$ holds for at most one $x$"?*
There is a somewhat analogous question for category-theoretic diagrams. I have seen the convention of using a dashed (or dotted) arrow to indicate the universality of the corresponding morphism (see, for example, Algebra by Mac Lane and Birkhoff). Some authors extend this convention to indicate existence-and-uniqueness (e.g. see Turi's Category Theory Lecture Notes). Hence, I see the dashed arrow as the "diagrammatic cousin" of $\exists\,!\,$. Now, suppose we are making some diagram $\mathcal{D}$ featuring objects $A$ and $B$, say.
Is there some convention to graphically represent the assertion "there is at most one morphism $\alpha$ from $A$ to $B$ [such that diagram $\mathcal{D}$ commutes]"?
Thanks!
*Of course, the immediate guess ("back-forming" from $\exists\,!$) is that the lone $!$ serves this purpose. Thus the assertion above would be expressed with $!\, x\!:\!P\,(x).$ I see no immediate problems with using $!$ for this purpose (with the possible exception of cases where the context includes many factorials) but I have never seen such usage, and I would prefer to adopt a notation that has at least some currency, even if it does not complement the $\exists\,!$ form as nicely as $!$ does.