[HoTT] A proof that univalence implies function extensionality

[Tslil Clingman <tslil@jhu.edu>]

[-- Attachment #1: Type: text/plain, Size: 1651 bytes --]

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 3410 bytes --]