index : univalence-to-funext

A derivation of function extensionality from the univalence axiom formalised in Agda

git repository hosting

about summary refs log tree commit diff

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

Write-up : PDF (LaTeX)

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

generated by cgit v1.2.3 (git 2.46.0) at 2026-08-30 07:26:50 +0000