index
:
univalence-to-funext
master
A derivation of function extensionality from the univalence axiom formalised in Agda
git repository hosting
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Univalence-to-funext.agda
Age
Commit message (
Expand
)
Author
2019-02-02
A proof that univalence implies function extensionality
tslil clingman