Initiality Project

The Initiality Project

The Initiality Project


The Initiality Project is a communal effort to prove an initiality theorem? for a dependent type theory: that the categorical structure constructed out of the syntax is the initial object in some category of structured categorical objects.

Plans and work

By type former

Jobs and volunteers

Here are the tasks to be done. To volunteer for a task, edit the page and put your name after it. Some tasks have many sub-tasks (e.g. each of the 8-ish rules at Initiality Project - Type Theory - Pi-types requires its own inductive clause at Initiality Project - Totality - Pi-types?), so feel free to split up the tasks listed below and volunteer at as small a level of granularity as you wish.

Page index

Last revised on March 11, 2019 at 08:37:21. See the history of this page for a list of all contributions to it.