This page contains supplementary material for the article "Work It, Wrap It, Fix It, Fold It".
A mechanical verification of the proofs in Agda is available as a tarball, or it can be browsed below as hyperlinked HTML (recommended).
CPO.agda — encoding of complete partial orders and continuous functions.
FixTheorems.agda — useful theorems about complete partial orders.
WWFix.agda — worker/wrapper transformation for least fixed points.
FoldTheorems.agda — useful theorems about folds.
FoldTheoremsInstantiated.agda — theorems about folds generated by instantiating the general categorical theory of initial algebras, where this differs from the above.
WWFoldCommon.agda — some definitions common to all of the following worker/wrapper transformations for folds.
WWFoldInstantiate.agda — worker/wrapper transformation for folds in CPO, by instantiating the general categorical theory.
WWFoldDerived.agda — worker/wrapper transformation for folds in CPO, derived from the worker/wrapper transformation for least fixed points.
WWFoldDirect.agda — worker/wrapper transformation for folds in CPO, proved from first principles.
Last updated 16th February 2016.