nLab Initiality Project - Term Model

Initiality Project - The Term Model

This page is part of the Initiality Project.

Base Theory

We define a category with families as follows:

• Its objects are the valid contexts. (Do we need to mod out by judgmental equality here?)
• Its types in context $\Gamma$ are the $A$ such that $\Gamma \vdash A\,type$ is derivable, modulo derivable judgmental equalities $\Gamma \vdash A\equiv B \, type$.
• Its terms of type $A$ in context $\Gamma$ are the $T$ such that $\Gamma \vdash T \Leftarrow A$ is derivable, modulo derivable judgmental equalities $\Gamma \vdash S \equiv T : A$.

TODO: prove that this defines a category with families.

Type formers

$\Pi$-types

TODO: Prove that the term model category with families has $\Pi$-type structure.

category: Initiality Project