uAgda

A simplistic dependently-typed language with parametricity.

uAgda implements an experimental dependently-typed language (and proof assistant by the Curry-Howard isomorphism), extended with support for parametricity.

See the share/tutorial directory for how to get started.