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}$).

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

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

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

Type theory