One counter automaton as a function
You can use the counter value as the result of the function.

Furthermore, if I understood well your question, a simple way to map $(bool,nat)$ is the following: modify the state transitions of the original automata $A$ to make the counter value equal to $2x$ if the counter of the original A is $x$ and the state is rejecting, $2x+1$ if the counter of the original $A$ is $x$ and the state is accepting.

If the one-counter machine that returns $(bool, nat)$ (with no distinction between accept/reject states, because the accept/reject condition is embedded in the returned value as explained above) is deterministic, then you can decide equivalence using this trick:

Given automata $M_1$, $M_2$ computing $f_1,f_2:\Sigma^* \to N \times \{0,1\}$;  you can transform them back to two standard accept/reject automata $M_1', M_2'$ computing $f_1',f_2':\Sigma^* \to \{0,1\}$.

Expand the alphabet adding an extra symbol $*$; and make $M_1'(x*^k ) = Accept$ if and only if $M_1(x) = k$.

When $M_1', M_2'$ find a $*$ they decrement the counter if it is $&gt;0$, otherwise they enter a permanent reject state. If the counter reaches $0$ after the decrement, then they enter an accept state. If they find another symbol after a $*$ they enter a permanent reject state.

Now you can check language equivalence of the "standard" one-counter automata $M_1', M_2'$ (decidable in the deterministic case, see L.G.Valiant, M.S.Paterson, Deterministic One-Counter Automata, 1975) and by construction $L(M_1') = L(M_2')$ if and only if $f_1 = f_2$.