All,
I hope this email finds you well. I'm writing to you today as i have formalised a proof that univalence implies function extensonality and i think this might be of at least positive interest here. This proof is unlike the `standard' one, as i discovered afterwards, in that it does not (obviously, anyway) factor through `weak function extensionality' and instead rather directly derives a witness for is-equiv(happly). My hope is that, either manifestly or through the write-up, this also feels like an `obvious' proof of the matter.
The Agda code and a short write-up can be found here
https://gitlab.com/tslil/univalence-to-funext
This small exercise arose on my part for two reasons:
1) I was not, at the time, aware of the details of such a proof and a good way to understand is to try for oneself.
2) I had not ever formalised anything before, and this felt like a foundational enough result that formalisation would be within grasp.
I expect that the second reason above readily shows in my code. I had had some difficulty in understanding the structure of the HoTT-Agda library and so i'm quite certain that i've duplicated work and taken unnecessary
detours -- i would be very glad to hear feedback about the implementation too!
Thanks for your time and consideration,
yours &c.,
tslil