~tslil/univalence-to-funext

710a808e23e2dac38ec4cb831679f63bcc71bec4 — tslil clingman 1 year, 6 months ago 5aefd67
Added README
1 files changed, 5 insertions(+), 0 deletions(-)

A README.md
A README.md => README.md +5 -0
@@ 0,0 1,5 @@
# A proof of UA -> funext, formalised in Agda

Writeup : [PDF](univalence-to-funext/tree/master/univalence-to-funext.pdf) ([LaTeX](univalence-to-funext/tree/master/univalence-to-funext.tex))

HoTT-Agda formalistion : [Univalence-to-funext.agda](univalence-to-funext/tree/master/Univalence-to-funext.agda)