A question about impredicative type theory

Question

I am playing with impredicative type theories (CC and UTT). I am not quite familiar with the distinction between $\textsf{Prop}$ and $\textsf{Type}$ as it is not available in MLTT. Here is my question.

Let $\Gamma$ be a valid context and let $A:\textsf{Prop}$, $D:\textsf{Type}$ and $B:D\rightarrow\textsf{Prop}$. My question can be divided into two parts:

1. By the above definitions, $A\rightarrow\Sigma x:D.B(x)$ is a well-formed type. Is it possible that $A\rightarrow\Sigma x:D.B(x)$ is not a theorem in an empty context but is a theorem in context $\Gamma$?
2. If $A\rightarrow\Sigma x:D.B(x)$ is not a theorem in an empty context but is a theorem in context $\Gamma$, then what amounts to a proof object of $A\rightarrow\Sigma x:D.B(x)$ in $\Gamma$?

Thanks!

Answer 1

$\newcommand{\Prop}{\mathsf{Prop}}$

If we take $P : \Prop$ to be some independent proposition, then we can take: $$A = ⊤\\D = 2\\B(0) = ¬P\\B(1) = P$$

Then a derivation of $$⊢ ⊤ → Σb:2. B(b)$$ is deciding $P$. If no non-constructive principles are assumed, presumably there is no such derivation. However there is an easy derivation of $$P ⊢ ⊤ → Σb:2.B(b)$$ In the sort of theories you're talking about, constructions in $\Prop$ aren't really very different from those in $\mathsf{Type}$, aside from rules for equality and possible restrictions on eliminators and the like. So a proof term could just look like:

$$p:P ⊢ λt. (1, p) : ⊤ → Σb:2.B(b)$$

I.E. propositional implication and $∀$ are proved by functions, $∧$ and $∃$ by pairs, and $∨$ by terms that look like they belong to a disjoint union, but values of a proposition are considered equal even if they are not syntactically identical, and e.g. you may not be able to do case analysis on an $∨$ value to produce a value of $A : \mathsf{Type}$.

Edit: perhaps I should mention, the bits about how $\Prop$ behaves differently are mostly unrelated to impredicativity, and are instead related to how people think propositions should be different from other types. The possible exception is that impredicative $Σ$ types are inconsistent unless you place restrictions on the way they are eliminated. However, I'm not sure the restrictions I mentioned above are the ones necessary to fix that problem.