Data Types as Quotients of Polynomial Functors, in lean 4

This is a port of avigad/qpf to lean 4. There it was described as

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.