The html is hyperlinked and highlighed, so it's nicer for reading, but download the agda if you want to play.


A slight generalization of Vladimir Voevodsky's proof that Univalence implies function extensionality. (With Martín Escardó)

    html
    agda

    A mini-library used in the proof: html; agda


An extension of Martín Escardó's proof that all System T definable functionals are continuous, to include coproducts.

    html
    agda


Agda formalization of NbE for combinatory System T (Coquand & Dybjer 1998; Dybjer &Filinski 2000)

    html
    agda

    mini-library: html; agda


back