Data Types as Quotients of Polynomial Functors.

Jeremy Avigad, Mario Carneiro, Simon Hudon

Browse the full ITP paper archive.