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

Plans and work

• Overview– currently a proposal, under discussion.
• Raw Syntax– Formally putting symbols together in a careful and well-defined way.
• Type Theory– The “type theory”, with rules on how to manipulate raw syntax. The usual notion of judgements with natural deduction.
• Semantics– Categorical structures used to model our type theory
• Partial interpretation function– How to arrive at the categorical model from our type theory
• Preservation of Substitution - Is substitution in the type theory the same as substitution in the semantics?
• Totality of the interpretation - Showing that the partial interpretation functions give rise to a total interpretation function (just a function).
• The Term Model
• The interpretation as a functor?
• Uniqueness of the interpretation functor
• References
• BibTeX database

By type former

• Initiality Project - Pi-types

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.

• Create skeletons for all the pages and list the tasks to be done (Mike Shulman)
• Define $\alpha$-equivalence and capture-avoiding substitution in Initiality Project - Raw Syntax (John Dougherty)
• Define a morphism of CwFs in Initiality Project - Semantics (Paolo Capriotti).
• Define $\Pi$-type structure on a CwF in Initiality Project - Semantics - Pi-types.
• Write out the equality rules at Initiality Project - Type Theory (Kenji Maillard?).
• Define signatures to give arities to constants, and write out the constant rules at Initiality Project - Type Theory.
• Write out the $\Pi$-type congruence rules at Initiality Project - Type Theory - Pi-types.
• Prove some admissible rules, etc. at Initiality Project - Type Theory.
• Define the partial interpretation on $\Pi,\lambda,App$ at Initiality Project - Partial Interpretation - Pi-types?.
• Prove local totality for the variable rule at Initiality Project - Totality.
• Prove local totality for the mode-switching rule at Initiality Project - Totality.
• Prove local totality for the equality rules at Initiality Project - Totality.
• Prove local totality for $\Pi,\lambda,App$ at Initiality Project - Totality - Pi-types?.
• Create, update and maintain a bibliography (Initiality Project - References), (Initiality Project - BibTeX database for the project and link it to existing material.
• QUESTION : whether geometric parametrized forms whose sense in sheaves is touched only grammatically is possible ?

Background links

• original nForum discussion
• n-Category Café announcement
• participant list. If you would like to participate, simply add your name to the list and join the conversation! All work will take place publically on nLab pages, nForum discussions, etc.

Page index

• Initiality Project
• Initiality Project - BibTeX database
• Initiality Project - Overview
• Initiality Project - Partial Interpretation
• Initiality Project - Participants
• Initiality Project - Pi-types
• Initiality Project - Raw Syntax
• Initiality Project - Raw Syntax - Pi-types
• Initiality Project - References
• Initiality Project - Semantics
• Initiality Project - Semantics - Pi-types
• Initiality Project - Substitution
• Initiality Project - Term Model
• Initiality Project - Term Model - Pi-types
• Initiality Project - Totality
• Initiality Project - Type Theory
• Initiality Project - Type Theory - Pi-types
• Initiality Project - Type Theory - Term equality
• Initiality Project - Type Theory - Type equality
• Initiality Project - Uniqueness

category: Initiality Project