This seemingly simple question is actually fairly deep, and leads quite directly to the "encode-decode method" used in HoTT to give synthetic proofs of classical theorems of algebraic topology. The key is to generalize the type of $f$. As you note, "$f(b,A_2)$" doesn't even make sense because $A_2$ doesn't have the correct type to be the second argument of $f$; but we need something analogous to "$f(b,A_2)$" in order to define $f$ by induction on $\mathsf{T}$.
Thus, instead of $f:\Pi_{b:\mathbf{2}} \mathsf{T}(0_{\mathbf{2}},b) \to (b=0_{\mathbf{2}})$, we will define $g:\Pi_{a:\mathbf{2}} \Pi_{b:\mathbf{2}} \mathsf{T}(a,b) \to P(a,b)$, where $P:\mathbf{2}\to \mathbf{2}\to \mathcal{U}$ is some type family such that $P(0_{\mathbf{2}},b) \equiv (b=0_{\mathbf{2}})$. Since the type of $g$ is more general, we will be able to use the induction principle for it; then we can define $f(b,t) = g(0_{\mathbf{2}},b,t)$.
How do we obtain $P$? By a recursion principle. In this case, that means case analysis on the first argument $a:\mathbf{2}$ of $P$. Our desired equality $P(0_{\mathbf{2}},b) \equiv (b=0_{\mathbf{2}})$ is the first case, and since we don't care about the other case we take it to be trivial to inhabit:
$$\begin{align*}
P(0_{\mathbf{2}},b) &:\equiv (b=0_{\mathbf{2}})\\
P(1_{\mathbf{2}},b) &:\equiv \mathbf{1}
\end{align*}$$
Now we can define $g$ by the induction principle of $\mathsf{T}$, with two cases corresponding to the two constructors of $\mathsf{T}$:
$$\begin{align*}
g(0_{\mathbf{2}},0_{\mathbf{2}},A_1) &:\equiv \mathsf{refl}_{0_{\mathbf{2}}}\\
g(1_{\mathbf{2}},b,A_2) &:\equiv \star
\end{align*}$$
Note that $g(a,b,t) : P(a,b)$ in both cases. Now, as noted above, we can define your $f:\Pi_{b:\mathbf{2}} \mathsf{T}(0_{\mathbf{2}},b) \to (b=0_{\mathbf{2}})$ by $f(b,t) = g(0_{\mathbf{2}},b,t)$.
This sort of trick, of defining a desired function by generalizing the domain and finding the codomain as a particular value of a recursively defined type family, is a fundamental way of characterizing inductively defined type families over inductive types, including particularly the identity type (in which case in HoTT it often goes by the name of the "encode-decode method"). It's introduced in sections 2.12 and 2.13 of the HoTT book for characterizing the identity types of coproducts and the natural numbers (in fact you need it even to prove that $0_{\mathbf{2}}\neq 1_{\mathbf{2}}$!), and then again in chapters 6 and 8 to study higher inductive types and compute homotopy groups of spheres.
Firstly, I would say that "assuming by path induction that $p\equiv \mathsf{refl}_x$ and showing the resulting identity holds" is "inhabiting a particular type". This is just a description in words of the identity-elimination rule, which is one of the basic term-formers of type theory and hence a way in which we inhabit types. But I take your meaning to be that you want to write down an explicit term.
Your first formulation is correct.
Your second formulation is close to mathematically correct, but since the output depends on the value of your $z:\sum_{x:A} P(x)$, the $\to$ needs to also be a $\Pi$. Also, in formal syntax, one would have to refer to the components $x$ and $u$ with the projection operators $\pi_1,\pi_2$ applied to $z$. So it would be
$$ \prod_{z:\sum_{x:A} P(x)} \prod_{y:A} \prod_{p:\pi_1(z)=y} z = (y, p_*(\pi_2(z))).$$
This is equivalent to your first translation, by the mapping-out universal property of $\Sigma$-types, equation (2.15.9) in the HoTT Book. However, I would tend to interpret the words as written in the book as referring to the first translation, since it gives separate names to $x$ and $u$ rather than a single name to $z$.
Best Answer
In section 2.2, it's noted that
and this is an instance of that. $\mathrm{pr}_1(\mathrm{lift}(u, p)) \equiv \mathrm{ap}_{pr_1}(\mathrm{lift}(u, p)): \mathrm{pr}_1(x, u) = \mathrm{pr}_1(y, p_*(u))$.