nLab Initiality Project - Pi-types

Initiality Project - $\Pi$-types

This page is part of the Initiality Project.

Here we collect all the rules, definitions, and inductive clauses that pertains specifically to $\Pi$-types.

Raw syntax

operator	sort	vars	type args	term args	scoping	sugared syntax
$\Pi$	$ty$	$x$	$A$, $B$		$B\lhd x$	$\Pi(x:A).B$
$\lambda$	$tm$	$x$	$A$, $B$	$M$	$B\lhd x$, $M\lhd x$	$\lambda(x:A.B).M$
$App$	$tm$	$x$	$A$, $B$	$M$, $N$	$B\lhd x$	$App^{(x:A).B}(M,N)$

Type theory

$$\begin{gathered} \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type}{\Gamma \vdash \Pi(x:A) .B \, type} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type \qquad \Gamma \vdash M \Leftarrow \Pi(x:A). B \qquad \Gamma \vdash N \Leftarrow A}{\Gamma \vdash App^{x:A.B}(M,N) \Rightarrow B[N/x]} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma,x:A \vdash B \,type \qquad \Gamma,x:A \vdash M \Leftarrow B}{\Gamma \vdash \lambda(x:A.B).M \Rightarrow \Pi(x:A). B} \\ \\ \frac{\Gamma\vdash A \equiv A' \, type \qquad \Gamma, x:A \vdash B \equiv B' \, type}{\Gamma \vdash App^{x:A.B}(\lambda(x:A'.B').M,N) \equiv M[N/x] : B[N/x]} \\ \\ \frac{\Gamma, y:A \vdash App^{x:A.B}(M,y) \equiv App^{x:A.B}(M',y) : B[y/x]}{\Gamma \vdash M \equiv M' : \Pi(x:A).B } \\ \\ \frac{\Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type}{\Gamma \vdash \Pi(x:A)B \equiv \Pi(x:A')B' type} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma, x:A \vdash M \equiv M' : B } {\Gamma \vdash \lambda(x:A.B).M \equiv \lambda(x:A'.B').M' : \Pi(x:A).B} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma \vdash M \equiv M' : \Pi(x:A)B \qquad \Gamma \vdash N \equiv N' : A } {\Gamma \vdash App^{x:A.B}(M, N) \equiv App^{x:A'.B'}(M', N') : B[N/x]} \end{gathered}$$

Semantics

include Initiality Project - Semantics - Pi-types

Partial interpretation

include Initiality Project - Partial Interpretation - Pi-types?

Preservation of substitution

include Initiality Project - Substitution - Pi-types?

Totality

include Initiality Project - Totality - Pi-types?

The Term Model

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

Interpretation functor

include Initiality Project - Functor - Pi-types?

Uniqueness

include Initiality Project - Uniqueness - Pi-types?

category: Initiality Project