I have rewritten my math book (volume 1) with implicit arguments (that is I sometimes write instead of to denote the least element of the lattice ).
It considerably simplifies the formulas.
If you want to be on this topic, learn what is called “dependent lambda calculus”. (Sadly, I do not use it in my book explicitly, in order to make my book easier to understand. But I weight the possibility to rewrite my book in a dependent lambda calculus proof-assistant language, that is in the language of an automatic proof verification software, to make it even greater.)