Fixed links
Added README
For some reason Agda could no longer infer for idp, added explicit
A proof that univalence implies function extensionality