@@ 1,5 1,5 @@
-# A proof of UA -> funext, formalised in Agda
+# A proof of UA -> funext, formalised in Agda-HoTT
-Writeup : [PDF](univalence-to-funext/tree/master/univalence-to-funext.pdf) ([LaTeX](univalence-to-funext/tree/master/univalence-to-funext.tex))
+Write-up : [PDF](univalence-to-funext.pdf) ([LaTeX](univalence-to-funext.tex))
-HoTT-Agda formalistion : [Univalence-to-funext.agda](univalence-to-funext/tree/master/Univalence-to-funext.agda)
+HoTT-Agda formalistion : [Univalence-to-funext.agda](Univalence-to-funext.agda)