~tslil/univalence-to-funext

ref: 710a808e23e2dac38ec4cb831679f63bcc71bec4 univalence-to-funext/README.md -rw-r--r-- 305 bytes
710a808e — tslil clingman Added README 1 year, 7 months ago

#A proof of UA -> funext, formalised in Agda

Writeup : PDF (LaTeX)

HoTT-Agda formalistion : Univalence-to-funext.agda