I will distinguish between mathematical functions and computational functions which I will think of for concreteness as $\lambda$-functions.
In every context I’ve encountered, the type signature of a lambda function depends only on its input-output relation. However, it seems to me that we can distinguish between two functions of the same input output types on the basis that they use a different set of types in their computation:
$f:\mathbb N\to \mathbb N \quad f=\lambda x:\mathbb N, (x+1)$
$g:\mathbb N\to \mathbb N \quad g=\lambda x:\mathbb N, (\text{toNat}\, (\text{toInt}\,x) + 1)$
Where $\text{toNat}:\mathbb Z \to \mathbb N, \text{toInt}:\mathbb N \to \mathbb Z$ do the obvious thing. (Note that $g$'s computations "depend on type $\mathbb Z$" but $f$'s do not).
In my own words, $f$ and $g$ have the same type signature but don’t have the same “type dependence” because $g$ depends on $\mathbb Z$.
Primary question: Is there a standard term for what I've called "type dependence"? Is there a standard theory of how to distinguish between $f$ and $g$ in terms of their “type dependence”?
Note: my question is not about "extentionality vs intentionality". See the comments.
—————
Secondary question:
I want to think about the difference between “type signature” and “type dependence” in categorical terms.
If we have morphisms (which we will think of as $\lambda$-functions) $f:A\to B$ and $g:B\to C$, then $g\circ f$ has type signature $g\circ f:A\to C$, but in a sense, the function $g\circ f$ has a type dependency on $B$.
Let’s say we have a $\lambda$-function $h:A\to C$, such that $h$ computes the same as $g\circ f$, which we will denote as an equivalence $h\equiv g\circ f$, but $h$ does not have a type dependence on $B$.
We want to be able to say: “the diagram containing $f,g,h$ commutes” while only referring to the equivalence in terms of "input-output equivalence" of $h$ and $g\circ f$, not their equivalence in terms of "type dependence".
Secondary question. Is there some kind of pre-existing theory within category theory about these things related to what I’ve been calling “type dependence”?
The standard categorical model of types and terms "forgets" a lot of information that it is reasonable for us to be interested in. It even renders equivalent all terms up to $\beta \eta$ equivalence, which sweeps all the difficulties of normalization, weak confluence under the rug and pretends they don't exist. So you may have a hard time finding categorical constructions where a morphism "remembers" all the objects that it passed through on the way; the usual impetus leads towards collapsing away all easily observed distinguishing features between "computationally equivalent" morphisms and coding the important information we want to use to reason about them into the domain and codomain.
If you plan to experiment with this, you could try using the "classifying space" of the category of types/terms, or the "nerve/realization" construction, to model your ideas. This would return a simplicial complex (or if you just want the combinatorial data, a simplicial set) where the sequence of morphisms $\lambda x:\mathbb N, (\text{toNat}\, (\text{toInt}\,x) + 1):\mathbb{N}\to\mathbb{N}\to \mathbb{Z}\to\mathbb{N}$ returns a three-dimensional simplex whose vertices are the types involved, the edges somehow represent the individual morphisms, and the composition of all of them somehow represents the whole simplex joining them all together.