I have rewritten my math book (volume 1) with implicit arguments (that is I sometimes write $latex \bot$ instead of $latex \bot^{\mathfrak{A}}$ to denote the least element of the lattice $latex \mathfrak{A}$).
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.)