Is path induction constructive?

Question

I'm reading through the HoTT book and I have a hard time with path induction.

When I look at the type in the section 1.12.1: $$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}} \left( \left(\prod_{x:A}C(x,x,\text{refl}_x)\right) \to \prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p) \right),$$ I have no issue understanding what that means (I just have written the type from memory, to check that).

What I have issue with is the next very statement:
$$\text{with the equality}\quad \text{ind}_{=_A}(C,c,x,x,\text{refl}_x):\equiv c(x)$$ my first impression was that this last expression does not define the resulting function $$f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$$ but just states its property.

That is in contrast to previous examples of the induction principles $\text{ind}_{A\times B}$,$\text{ind}_{A+B}$ or $\text{ind}_\mathbb{N}$ -- there are defining equations for those elements -- we actually know how to construct the resulting function, given the premises. Which is in agreement with the "constructiveness" of type theory adverted throughout the chapter.

Going back to $\text{ind}_{=_A}$, I was suspicious about the fact that (looks like) it is not defined. Stating that the element $f$ just exists seemed out of tune with the rest of the chapter. And indeed, the section 1.12.1 seems to stress that my impression is wrong and we in fact have defined

... the function $f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$ defined by
path induction from $c:\prod_{x:A}C(x,x,\text{refl}_x)$, which moreover
satisfies $f(x,x,\text{refl}_x):\equiv c(x)$ ...

That leaves me utterly confused, but I have a feeling that this point is very important for all the further developments. So which of the two readings for $\text{ind}_{=_A}$ should I go with? Or, probably, I'm missing some important subtlety and the answer is "neither"?