Agda embraces Unicode. PureScript & Haskell (with the UnicodeSyntax extension) both behave pretty well with a lot of Unicode operators (but rely on bicameral scripts as the leading character for deciding if something like a value or a Constructor/Type). Not sure of its status, but ocaml-m17n is a way to get some Unicode support in OCaml which otherwise can’t deal with any of it.