Lemma 2.3.2 of the HoTT book states a path lifting property.
I want to give a formal proof, in the sense that I want to inhabit a particular type, rather than just assume by path induction that $p \equiv refl_x$ and show the resulting identity holds.
So let's start by writing out the type corresponding to the proposition. If I wanted to be extremely verbose I would preface the following type with $\Pi_{A : \mathcal{U}} \Pi_{P:A \to \mathcal{U}}…$ but I realize that I can just construct what follows and curry it appropriatly to arrive at an element of the more verbose type. So GIVEN $A: \mathcal{U}$ and type family $P:A \to \mathcal{U}$ (I think) the HoTT book wishes us to inhabit:
$$\Pi_{x:A} \Pi_{u:P(x)} \Pi_{y:A} \Pi_{p:x=y} (x,u)=(y,p_*(u)) $$
the ordering here is determined by the wording of the Lemma, but one can show that this type is logically equivalent to:
$$\Pi_{x,y:A} \Pi_{p:x=y} \Pi_{u:P(x)} (x,u)=(y,p_*(u)) $$
(you simply defines functions in both directions that shift arguements around.)
This is what I think the HoTT book intends to be proven. But I think the wording of the Lemma is a bit ambiguous. On my first translation I ended up with:
$$ \Sigma_{x:A} P(x) \to \Pi_{y:A}\Pi_{p:x=y} (x,u)=(y,p_*(u)) $$
because I was interpreting, "assume we have $u:P(x)$ for some $x:A$" from the Lemma to mean if we have $z:\Sigma_{x:A} P(x)$ where $z \equiv (x,u)$.
Is one or both of these translations incorrect?
I have a formal proof, in the sense that I specified early, of the first translation but not the second.
Best Answer
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$.