README.md


1
2
3
4
5

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

Writeup : [PDF](univalence-to-funext/tree/master/univalence-to-funext.pdf) ([LaTeX](univalence-to-funext/tree/master/univalence-to-funext.tex))

HoTT-Agda formalistion : [Univalence-to-funext.agda](univalence-to-funext/tree/master/Univalence-to-funext.agda)