Does the "propositions-as-type" paradigm matches mathematical practice? Or is logic in mathematical practice a layer beneath mathematics, and mathematics built on top? For example, should we distinguish between the meta-"or" (which we use when formulating theorems) and the function $\mathrm{Bool}\times\mathrm{Bool}\to\mathrm{Bool}$ on $\mathrm{Bool}:=\{0, 1\}$ that maps $(p, q)$ to $\mathrm{max}(p, q)$?

I think that in classical foundations such as FOL+ZFC, logic is a separated layer, but in modern foundations of mathematics such as type theory, the logical connectives which we are use when formulating theorems are themselves mathematical objects. Is that true?