Category theoretic morphism definition syntax, e.g.: $\varphi : G \to H$ uses the colon character rather than, for instance, the member-of sign e.g.: $\varphi ∈ G \to H$
What is the descriptive name of colon in this context? What is the semantic gain of this additional entity over member-of?
On
The colon “:” generally abbreviates a pair of equalities.
A category is generally defined as consisting of things called ‘objects’ and ‘morphisms’ --as well as other things-- such that: Each morphism $f$ has an associated “source” object and an associated “target” object.
To avoid being verbose, a syntactic construct is introduced: $$ f : A → B \qquad≡\qquad \mathsf{source}\,f \,=\, A \;\;\land\;\; \mathsf{target}\,f \,=\, B $$
Hope that helps :-)
The colon is a typing symbol and does not represent equality.
The assertion $\varphi : G \to H$ asserts that $\varphi$ is a morphism from the object $G$ to the object $H$. There may be many different morphisms from $G$ to $H$, so replacing $:$ by $=$ would not make much sense.
There are instances when a morphism is understood from context, when you might write an $=$ sign. For example, if you see something like:
What is probably meant is that $1$ is a terminal object in a category $\mathcal{C}$ and $f$ is the unique morphism from $A$ to $1$ in $\mathcal{C}$.
Related note: in the branch of type theory, the colon is used more widely; the notation $a : A$ represents the assertion that a term $a$ has type $A$. In type theory, the notation $A \to B$ represents a function type, and then a function $f : A \to B$ truly is a term $f$ of type $A \to B$.