# nLab Initiality Project

The Initiality Project

# The Initiality Project

## Overview

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.

## 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.