===== Dependent type theory =====
==== Framework ====
We want dependent types together with type constructors
$$\Pi,\ \Sigma,\ \to,\ \times,\ +$$
and basis types
$${\bf 0},\ {\bf 1},\ {\bf 2}$$
Moreover some type definition schema alla **algebraic data types** and/or **(higher) inductive types** and/or **W-types** etc. For example, $\mathbb N$ is nicely inductively defined via successor function (using $\to$), or as [[initial algebra]] for a type former (using $+$ and ${\bf 1}$).

=== Dependent types and their geometrical interpretation ===
The introduction of quantifiers can be geometrically understood as follows:

$\large\frac{(\Gamma,x\,:\,A)\ \vdash\ Q\,:\,\mathrm{Type}}{\Gamma\ \vdash\ \Pi_{x:A}Q\,:\,\mathrm{Type}}$ 
$\hspace{.5cm}\Longleftrightarrow\hspace{.5cm}$
$\large\frac{\text{If over any base point $x:A$, we can construct a fibre $Q(x)$}}{\text{then we can set up a fibre bundle with section space $\Pi_{x:A}Q(x)$}}$

$\large\frac{(\Gamma,x\,:\,A)\ \vdash\ q\,:\,Q}{\Gamma\ \vdash\ s\,:\,\Pi_{x:A}Q}$ 
$\hspace{.5cm}\Longleftrightarrow\hspace{.5cm}$
$\large\frac{\text{If over any base point $x:A$ and fibre $Q(x)$ we can construct a value $q(x):Q(x)$}}{\text{then we can set up a section $s:\Pi_{x:A}Q(x)$}}$

The same thing goes for the "total space" and $\Sigma$. 

==== Discussion ====
=== Redundancies of the type formers ===
From a minimalist pov, we only need the type constructors
$$\Pi,\ \Sigma$$
and basic types 
$${\bf 0},\ {\bf 2}$$
Then 

  * $\to$ can be taken as $\Pi$ when the quantified expression is constant, $A\to B:=\Pi_{x:A}B$

  * $\times$ can be taken as $\Sigma$ when the quantified expression is constant $A\times B:=\Sigma_{x:A}B$

  * $+$ can be taken as $\Sigma$ over ${\bf 2}$, here we need an if-construction

  * ${\bf 1}$ can be taken as ${\bf 0}\to{\bf 0}$, since $\lambda x.x$ is a term of this type

One could also drop ${\bf 2}$ in favour of $+$, because 

  * ${\bf 2}$ can be taken as ${\bf 1}+{\bf 1}$

On the level of cardinalities, these idendifications manifest themselves as follows

  * $\prod_{n=1}^NP=P^N$

  * $\sum_{n=1}^NP=N\times P$

  * $\sum_{n=1}^2P(n)=P(0)+P(1)$

  * $0^0=1$

  * $1+1=2$

Lastly, let's note that if one allows for rule schemas, then one really only needs dependent products and inductive types (and a universe of types).

== Characterization of $\Pi,\Sigma$ as adjoints ==
The above construction "$\frac{input}{output}$" is in fact the object map of a functor and the introduction is right adjoint to the (pullback of the!) "weakening" of context, where one simply keeps track of an additional term:

$\large\frac{\Gamma\ \vdash\ p\,:\,P}{(\Gamma,x\,:\,A)\ \vdash\ (x\,:\,A,p\,:\,P)}$
 
Recall the standard adjunction example (currying)

$\mathrm{Hom}\left(A\times P,Q\right) \cong \mathrm{Hom}\left(P,A\to Q\right)$

For fibrations we have a somewhat similar adjunction, except we must keep track of the $x$-dependent codomains. Roughly

"$\mathrm{Hom}\left((x:A,p:P),(q(x):Q(x))\right) \cong \mathrm{Hom}\left((p:P),(s:\Pi_{x:A}Q(x))\right)$"

The bijection is established (right to left) by evaluation at the argument $x$ from the weakening functor, a map sending $(p:P)$ to $(s:\Pi_{x:A}Q(x))$ can be made into a map sending $(x:A,p:P)$ to $(s(x):Q(x))$ and (left to right) by lambda abstraction. 

The nats of the adjunction are then important type theoretic operations ($\beta$-reduction, etc.)

=== Reference ===
==== Parents ====
=== Related ===
[[Type theory]]