Comment by nxobject

And, if you think the wrapper $type_expr! is too verbose, just use [blackboard bold M](...) or something.

Agda is my favorite example of a language that _judiciously_ uses Unicode symbols to express "concepts similar to something but is actually substantially different so let's not get them confused"... as opposed to other theorem proving languages of its time [1]

[1] https://people.inf.elte.hu/divip/AgdaTutorial/Functions.Equa...