Abbrev used before introduced

Suggested solution

Line 805 in 1ac9408

in $\sm{x:A}P(x)$, such that $\ap{\proj1}{\mathsf{lift}(u,p)} = p$.

pr_1 is applied on the identity type instead of product type. Should it be $\apfunc{\proj1}(\mathsf{lift}(u,p)) = p$ ? So are the follows.

book/basics.tex

Lines 849 to 851 in 1ac9408

    
           Given $f:\prd{x:A} P(x)$, we can define a non-dependent function $f':A\to \sm{x:A} P(x)$ by setting $f'(x)\defeq (x,f(x))$, and then consider $\ap{f'}{p} : f'(x) = f'(y)$. 
        
           Since $\proj1 \circ f' \jdeq \idfunc[A]$, by \cref{lem:ap-functor} we have $\ap{\proj1}{\ap{f'}{p}} = p$; thus $\ap{f'}{p}$ does ``lie over'' $p$ in this sense. 
        
           However, it is not obvious from the \emph{type} of $\ap{f'}{p}$ that it lies over any specific path in $A$ (in this case, $p$), which is sometimes important.

Origin

After change

In section 2.4, it states f(p) is the same as ap_f(p). But I think it is confusing to use an abbrev before it is introduced.

The abbreviation is introduced in section 2.2, after the proofs of Lemma 2.2.1.

The abbreviation is introduced in section 2.2, after the proofs of Lemma 2.2.1.

Actually, it is introduced here.

book/basics.tex

Line 1024 in 1ac9408

    
           Recall that for $f:A\to B$ and $p:\id[A]xy$, we may write $\ap f p$ to mean $\apfunc{f} (p)$.

When I continued to read the book, I found it's not a typo but a use before introduction. However, it made me confusing. And I believe someone else may encounter the same problem.

Here's what Mike was referring to:

Right. The line in section 2.4 you point to says "Recall" because it is reminding the reader of a notation that was introduced previously.

Here's what Mike was referring to:

Oh, I miss it. Thanks. I'll close the issue.

	Given $f:\prd{x:A} P(x)$, we can define a non-dependent function $f':A\to \sm{x:A} P(x)$ by setting $f'(x)\defeq (x,f(x))$, and then consider $\ap{f'}{p} : f'(x) = f'(y)$.
	Since $\proj1 \circ f' \jdeq \idfunc[A]$, by \cref{lem:ap-functor} we have $\ap{\proj1}{\ap{f'}{p}} = p$; thus $\ap{f'}{p}$ does ``lie over'' $p$ in this sense.
	However, it is not obvious from the \emph{type} of $\ap{f'}{p}$ that it lies over any specific path in $A$ (in this case, $p$), which is sometimes important.