univalence-to-funext/univalence-to-funext.tex, branch masterA derivation of function extensionality from the univalence axiom formalised in Agdahttps://git.l-3.space/univalence-to-funext/atom?h=master2019-02-03T00:57:05ZA proof that univalence implies function extensionality2019-02-03T00:57:05Ztslil clingman2018-09-19T03:59:12Zurn:sha1:dd01e956d2a3d05597113a7c454ac4cb09e3ec19