~tslil/univalence-to-funext

A derivation of function extensionality from the univalence axiom formalised in Agda
35576e52 — tslil clingman 5 years ago 
Fixed links
710a808e — tslil clingman 5 years ago 
Added README
5aefd676 — tslil clingman 5 years ago 
For some reason Agda could no longer infer for idp, added explicit

refs

master
browse  log 

clone

read-only
https://git.sr.ht/~tslil/univalence-to-funext
read/write
git@git.sr.ht:~tslil/univalence-to-funext

You can also use your local clone with git send-email.

#A proof of UA -> funext, formalised in Agda-HoTT

Write-up : PDF (LaTeX)

HoTT-Agda formalistion : Univalence-to-funext.agda