> It is both, in the same way as a function is both its implementation and its "extension" (its effect on all inputs).

Note that, according to definition of 'function' most common in math, this is false. A function need not even be implementable.

Aside: As someone trained in math I've always found explanations of type theory "fractally confusing" because of stuff like this: type theorists' words mean something different from my words, and in the explanation of what they do mean, they use words that also mean something different.