I have a question about a certain method of proof used in the HoTT book. This question might just boil down to how univalence is used in practice. The method of proof I have in mind can be seen in one of the first steps of lemma 4.1.1 in the HoTT book. I will copy the relevant text:
''Lemma 4.1.1. If $f : A \to B$ is such that $qinv( f )$ is inhabited, then $qinv( f ) \simeq ( id_A\sim id_A )$
Proof. By assumption, f is an equivalence; that is, we have $e : isequiv( f )$ and so $( f , e) : A \simeq B$. By univalence, $idtoeqv : ( A = B) \to ( A \simeq B) $is an equivalence, so we may assume that $( f , e)$ is of the form $idtoeqv( p)$ for some $p : A = B$. Then by path induction, we may assume $p$ is $refl_A$ , in which case $idtoeqv(p)$ is $id_A$ …''
I don't quite understand how we are able to use path induction after applying univalence. My understanding of the lemma and the structure of the proof is the following:
For types $A$ and $B$ we want to inhabit $\prod_{f:A\to B}qinv(f)\to (qinv(f)\simeq(id_A \sim id_A))$. The authors then augment the context with $f:A\to B$ and $q:qinv(f)$, and then seek to inhabit $(qinv(f)\simeq(id_A \sim id_A))$. From $q:qinv(f)$, we can derive $e:isequiv(f)$. It follows that $(f,e):A\simeq B$. By the computation homotopy for univalence, $idtoeqv(ua(f,e))=(f,e)$, where $ua(f,e):A=B$. Thus, $(f,e)$ is of the form $idtoeqv(p)$, for some $p:A=B$. Now, and here is where I get stuck, the authors of the book go on to apply path induction to $p$. But, my understanding of applying (based) path induction is that it reduces the task of constructing a term of $\prod_{x:A}\prod_{p:a=x}C(x,p)$ to the task of constructing a term of $C(a,refl_a)$. But, in this lemma, we are not looking to construct a term of the form $\prod_{x:A}\prod_{p:a=x}C(x,p)$. In the current context, we are looking to construct a term of $(qinv(f)\simeq(id_A \sim id_A))$.
So, it doesn't seem like we can just directly apply path induction. I spent some time thinking about how to make sense of this and I came up with to possibilities:
(i) Keeping the same context, first construct a term $H:\prod_{p: A=B} (qinv(idtoeqv(p))\simeq(id_A \sim id_A))$ using path induction. Then, we use the fact that $idtoeqv(ua(f,e))=(f,e)$ and $H(ua(f,e)):(qinv(idtoeqv(ua(f,e)))\simeq(id_A \sim id_A))$ to derive an inhabitant of $qinv(f,e)\simeq(id_A\sim id_A)$. Then we may discharge the added assumptions in our context to derive a term of $\prod_{f:A\to B}iseqv(f)\to (qinv(f)\simeq(id_A \sim id_A))$.
or (ii) in this method, the proof starts without augmenting the context. Instead, notice that goal in lemma 4.1.1 is to inhabit $\prod_{f:A\to B}qinv(f)\to (qinv(f)\simeq(id_A \sim id_A))$. Since $qinv(f)\leftrightarrow isequiv(f)$, it suffices to inhabit $\prod_{f:A\to B}isequiv(f)\to(qinv(f)\simeq(id_A \sim id_A))$. But this latter type is equivalent to the type $\prod_{(f,e):A\simeq B}qinv(f)\simeq(id\sim id)$. By univalence, $idtoeqv:(A=B)\simeq(A\simeq B)$, so the previous type is equivalent to $\prod_{p:A=B}qinv(idtoeqv(p))\simeq(id\sim id)$. Now we can apply path induction.
The reason I ask is because the latter method seems better but this latter method requires results about how type constructors preserve equivalence, namely the results of exercise 2.17. However, exercise 2.17 ask the reader to derive the results in two ways: one using univalence and one not. So, how does the proof of exercise 2.17 use univalence? It seems like it can't use method (ii) since that would require already having the proof of 2.17.
So my question is twofold: how is lemma 4.1.1 in the HoTT book using univalence, method (i) or (ii)? If the book is using method (ii), how then is univalence used in the proof of exercise 2.17? Sorry for the long post, thanks in advance.
Best Answer
I think the intent when we wrote it was method (i), but method (ii) works as well. When formalizing in a proof assistant, one might indeed choose method (ii) as better for some reasons.
For exercise 2.17, I think the idea for the univalence-using proof was much simpler: just use the equivalence $(A\simeq A') \simeq (A=A')$ directly, since in this case there is no dependency to worry about.