aboutsummaryrefslogtreecommitdiff
path: root/Univalence-to-funext.agda
AgeCommit message (Expand)Author
2019-02-02For some reason Agda could no longer infer for idp, added explicittslil clingman
2019-02-02A proof that univalence implies function extensionalitytslil clingman