Data Types as Quotients of Polynomial Functors

This repository contains a formalization of data type constructions in Lean, by Jeremy Avigad, Mario Carneiro, and Simon Hudon. A preliminary version of the work is described in this talk: http://www.andrew.cmu.edu/user/avigad/Talks/qpf.pdf.

See src/README.md for a description of the contents.

The easiest way to test the code is as follows:

• Install a precompiled binary of Lean.

• In the root folder of this repository, type

        path-to-lean/bin/leanpkg build
  

  where path-to-lean is the path to the folder you just installed.

This will install a local copy of the mathlib and compile and check the dependencies as well. Lean will report any errors or sorrys. (There shouldn't be any.)

If you want to browse the files with interactive feedback from Lean, we recommend using Visual Studio Code and installing the Lean extension via the extension manager.

There are variations. For instructions that install elan, a system which will manage versions of Lean for you automatically, see here. You can also install mathlib via binaries, following the directions in the README file here.

To test the data type compiler, see test/README.md.