typo in commit

[andreykl]

I think there is a typo in the commit 7606d81

this is removed from the line 1421

 For example, with univalence, we will be able to show $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$, although $\bfalse \neq_{\bool} \btrue$.

and the on the line 2694 we have

We have seen that $\bfalse \neq \btrue$ (\cref{rmk:false-neq-true}). Show that, nevertheless, $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$ (see \cref{rmk:sigma-equality-extraction}).

But we do not see this anymore since we just removed it (from line 1421). And there is no label false-neq-true anywhere in the book except this place according to github search.

[mikeshulman]

What was removed was not the observation that $\bfalse \neq \btrue$, but that $(\bool, \bfalse) =_{\sm{A:\type}A} (\bool, \btrue)$, which was moved to this exercise in #1171. However, you're right that the reference to rmk:false-neq-true is wrong; it should be rmk:true-neq-false.