This repository contains the Coq formalization of the results in the paper "Homotopy-Initial Algebras in Type Theory" by Steve Awodey, Nicola Gambino, and Kristina Sojakova, available at http://arxiv.org/abs/1504.05531.
The repository contains two files:
The file "two.v" contains the formalization of the results found in chapters 2 and 3 of the paper ("Bipointed Types" and "Homotopy-Initial Bipointed Types").
The file "w.v" contains the formalization of the results found in chapters 4 and 5 of the paper ("Polynomial Functors and Their Algebras" and "Homotopy-Initial Algebras").
The files use the Coq Homotopy Type Theory (HoTT) library, found at https://github.com/HoTT/HoTT. They are confirmed to run under commit a4658e60995ff7c841c7f70157d24cd85d418878 of the master branch, April 20, 2015, but are likely to work under any subsequent commits as well.
The HoTT library comes with a pre-packaged version of the Coq system, so no separate installation of the latter is required. For further instructions please refer to https://github.com/HoTT/HoTT/blob/master/INSTALL.md.