type theory - What is a semigroup or, what do I do with that associativity proof?

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S times S rightarrow S$. So far, so good.

From a computational perspective, one can represent a semigroup as the tuple $left< S,* right>$, or my preference, as a record { S: type; $* : S times S rightarrow S$} which is dependently typed. So, for example, {S = $mathbb{N}$; $* = + $} is a semigroup [assuming I have the naturals with addition already built].

Well, actually, it's not -- who says that I defined $+$ properly? Maybe I made a mistake and the $+$ that I used for $mathbb{N}$ isn't associative. So I sure shouldn't be able to build {S = $mathbb{N}$; $* = + $} and have that have 'type' semigroup.

So is the proof of associativity part of the type 'semigroup' (as it is in Coq for example), or is it part of the input to the 'constructor' for the semigroup type ? [The constructor is allowed to then forget the proof, at least for computational purposes].

One wrinkle here is that while the proof of associativity doesn't seem to say much, for the term algebra over the semigroup, it does induce two 'associator' functions which can perform the rewrite of $lceil a * (b * c) rceil leftrightarrow lceil (a * b) * crceil$ (where I use the $lceil cdot rceil$ brackets to denote working over terms since semantically $a*(b*c)$ and $(a*b)*c$ denote the same thing so there is nothing to do). That associator is really quite useful [and much more so when you go to things like rings and fields, where the induced rewrites on the term algebra give rise to what can rightly be called a 'simplifier']. So the proof is quite useful in that sense.

The question boils down to: where does the 'proof' that the binary operation is associative really belong in the theory of a single semigroup, where by 'theory' here I mean both the semantic theory and the induced equational theory of the term algebra? Once I have established that $*$ is associative, can I really throw away the proof as it is not going to be used again?

(I would really want to also ask why is it that in classical mathematics, proofs are crucial, but somehow not so important that definitions of standard objects omit them. Asking that would likely be ruled as off-limits for MO as being too 'philosophical'...)