In our daily use of math, it seems to me that we are allowing introduction of functional predicates into the language system. For instance, the formula \begin{equation} \forall x \in \mathbb{R}, \int_{0}^{x}t\mathrm{d}t = \frac{x^{2}}{2} \end{equation} is of two explanations. In the first explanation, we have \begin{equation} \forall x \in \mathbb{R}, \forall y, P\left(y,f,x\right) \Longrightarrow y = \frac{x^{2}}{2}, \end{equation} where I have omitted the formula specifying $f\left(t\right) = t$ (universal quantification on $f$ if expanded in the formula) and of course, the definition for division. Further $P$ is a predicate about the definition of integral from $0$. Of course, this type of language is very verbose. In my understanding, most people think of the equation the second way: \begin{equation} \forall x \in \mathbb{R}, \operatorname{I}\left(f,x\right) = \frac{x^{2}}{2}, \end{equation} where $\operatorname{I}$ is a functional predicate for integral introduced after we proved that for each $x \in \mathbb{R}$, the integral of any integrable function $f$ from $0$ to $x$ is unique. From this example, I guess we are implicitly allowing introduction of predicate functions in our daily use of math, even without notice. Is this correct?
P.S. I am not sure if it is normal feeling. I have long been upset from childhood by the fact that most of us (of course including me) are using math without knowing the bottom mechanisms of logical system (like in this case, probably we are not sure about rules of type theory while we are using it). It is like a programmer writes code without knowing hardware behavior. In particular, we are using high-level language, so that even without knowing much about hardware, we can still come up with correct implementations. But there is huge uncertainty when we are using something we don't really know from bottom up, and this uncertainty sometimes causes frustration. In real life, for survival purposes, we have to refrain from understanding these seemingly trivial, but in fact important things. For instance, as researchers, if we keep thinking and learning about this knowledge, we will not be able to focus on generating publications, and will not be highly rated in the academic system. If we focus on practical studies, we are not able to understand the bottom mechanism of thinking. Kind of a dilemma for scholars.