A relational symbol representing type declarations or definitional equality in type theory and formal logic.
Examples
Type declaration in type theory
x \dblcolon \text{Int}
Function type signature
map \dblcolon (a \to b) \to [a] \to [b]
Category theory morphism typing
f \dblcolon A \to B \text{ in } \mathcal{C}