You can clone with
HTTPS or Subversion.
In the last para of the proof of Lemma 6.4.2, I'd suggest to replace the appeal to function extensionality by: By contraposition of happly (2.9.2), it suffices for ... to show that ...
(Feel free to ignore this issue if it is deemed too minor.)
Actually, I'm not sure "overkill" is the right word; funext is literally going the wrong way for what we need here.
Yes. But "function extensionality" postulates "happly is an equivalence", so with some good will one could take it to refer to happly. Dissecting the "good will", if you say P(a) for a type family P over A, you imply a:A. It is better to state this directly, if a:A is all that is needed.
Anyway, thanks for the fast response (that I see did come already)!
6.4.2 isn't using funext, close #640