# What is $Prop$ in the calculus of constructions?

I'm looking at the Calculus of Constructions and its place in the Lambda Cube.

If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the simply-typed calculus, $\lambda_\to$. The first axis adds type-to-term operators, the second type-to-type operators, and the third dependent typing, or term-to-type operators. The CoC has all three.

However, the CoC introduces a term $Prop$, and states that $Prop : Type$ by the inference rules, but is otherwise not used. I understand that it is for the eponymous propositions, but the logical propositions are not defined in terms of it.

Could you explain to me what $Prop$ is for, where/when it appears, and explain it in terms of the cube's axes (if indeed it is possible to do so)?

There are many variants of CoC, but most would have $$\mathsf{Prop} : \mathsf{Type}$$ but not $\mathsf{Type} : \mathsf{Prop}$. Another difference shows up when we have infinitely many type universes and make $\mathsf{Prop}$ impredicative (this is what Coq does). Concretely, consider a variant of CoC where we have $\mathsf{Prop}$ and infinitely many type universes $\mathsf{Type}_1$, $\mathsf{Type}_2$, $\mathsf{Type}_3$ with \begin{align*} \mathsf{Prop} &: \mathsf{Type}_1 \\ \mathsf{Type}_1 &: \mathsf{Type}_2 \\ \mathsf{Type}_2 &: \mathsf{Type}_3 \\ &\vdots \end{align*} The formation rule for $\prod$ has to explain how to form $\prod_{x : A} B(x)$ when $A$ is either a proposition or a type, and $B(x)$ is either a proposition or a type. There are four combinations:
1. $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
2. $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Prop}} {\prod_{x : A} B(x) : \mathsf{Prop}}$$
3. $$\frac{A : \mathsf{Prop} \qquad x : A \vdash B(x) : \mathsf{Type}_i} {\prod_{x : A} B(x) : \mathsf{Type}_i}$$
4. $$\frac{A : \mathsf{Type}_i \qquad x : A \vdash B(x) : \mathsf{Type}_j} {\prod_{x : A} B(x) : \mathsf{Type}_{\max(i,j)}}$$
The most interesting is the difference between the second and the fourth case. The fourth rules says that if $A$ is in the $i$-th universe and $B(x)$ is in the $j$-th universe, then the product is in the $\max(i,j)$-th universe. But the second rule is telling us that $\mathsf{Prop}$ is not just "one more universe at the bottom", because $\prod_{x : A} B(x)$ lands in $\mathsf{Prop}$ as soon as $B(x)$ does, no matter how big $A$ is. This is impredicative because it allows us to define elements of $\mathsf{Prop}$ by quantifying over $\mathsf{Prop}$ itself.
A concrete example would be $$\prod_{A : \mathsf{Type}_1} A \to A$$ versus $$\prod_{A : \mathsf{Prop}} A \to A$$ The first product lives in $\mathsf{Type}_2$, but the second one is in $\mathsf{Prop}$ (and not in $\mathsf{Type}_1$, even though we are quantifying over an element of $\mathsf{Type}_1$). In particular, this means that one of the possible values for $A$ is $\prod_{A : \mathsf{Prop}} A \to A$ itself.