Lemma 2.3.2 of the HoTT book defines a kind of path-lifting for "fibrations" (ie type families):enter image description here

The proof is left as an exercise, but I'm struggling to understand what the last propositional equality means. The main body of the lemma is straightforward; indeed, by induction on $p$ we may assume $p\equiv\text{refl}_x$, and then take $\text{lift}(u, \text{refl}_x)\equiv \text{refl}_{(x, u)}$. Since $(\text{refl}_x)_*\equiv \text{id}_{P(x)}$ this is evidently well-typed, and hence by the induction principle will induce the desired function $\text{lift}:\Pi_{u:P(x)}\Pi_{p:x=_A y}(x, u)=(y, p_*(u))$. (Though really to be very formal I think we would want to first define $\text{lift}':\Pi_{p:x=_A y}\Pi_{u:P(x)}(x, u)=(y, p_*(u))$ by induction and then define $\text{lift}$ by swapping the arguments in $\text{lift}'$.) In any case this is fine to me. But I don't see why it now makes sense to apply $\text{pr}_1$ to $\text{lift}(u, p)$...

Surely to reason about such an application we would need the identity type $(x, u)=_{\Sigma_{(z:A)}P(z)}(y, p_*(u))$ to be somehow (judgementally equal to?) a dependent sum type; it would have to be of shape $\Sigma_{x=_A y}B$, but I am not sure what to substitute in for $B$. Intuitively we would want $B$ to be a (dependent) "space of paths" between $u$ and $p_*(u)$ (parametrized by the first coordinate $p$), but since $u:P(x)$ and $p_*(u):P(y)$ it is not clear how to make sense of such a space. Even if there were a suitable choice for $B$, I don't see how to make such an identification formal; surely an identity type and a dependent sum type cannot be judgmentally equal. Can anyone help clear up this confusion?


1 Answer 1


In section 2.2, it's noted that

We will often write $\mathrm{ap}_f(p)$ as simply $f(p)$

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))$.

  • $\begingroup$ Ah, of course; stupid mistake. Thank you $\endgroup$ Mar 14, 2020 at 21:13
  • 4
    $\begingroup$ FWIW, in the years since we wrote the book I've come to believe that that abuse of notation is more confusing than useful, and if there is ever a second edition I'll probably advocate for always writing the "ap". $\endgroup$ Mar 15, 2020 at 16:41
  • 2
    $\begingroup$ No, there are no plans. $\endgroup$ Apr 13, 2021 at 19:49

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .