agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.