Iowa Type Theory Commute
More about the structured recusion scheme known as the catamorphism. Basic idea of functors.