Small Induction Recursion, Indexed Containers and Dependent Polynomials are equivalent

Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock and Conor McBride

This URL is also a darcs repository. To take a local copy of the repository, feel free to

darcs get http://personal.cis.strath.ac.uk/~conor/pub/SmallIR

You may also access the literate Agda source of this paper. The full .pdf including appendices are also available.