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

Write-up : [PDF](univalence-to-funext.pdf) ([LaTeX](univalence-to-funext.tex))

HoTT-Agda formalistion : [Univalence-to-funext.agda](Univalence-to-funext.agda)