This repository contains a cleaned up version of the work done in Nottingham under Thorsten Altenkirch's supervision.
It is based on Amine Chaieb and Tobias Nipkow's formalization of a similar procedure in HOL.
This development has been typechecked with Agda version 2.6.0, using various extensions of the standard library currently waiting to be merged.