# A question about impredicative type theory

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!

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

• Hi, a quick question. What do you mean by requiring $D=2$? Or you mean $D$ is $\textsf{Bool}$? Because I see later you mention 0 and 1. Thanks! – Samuel Jan 14 at 10:52
• Yeah, I mean the type with two values. Could be $\mathsf{Bool}$, $\mathsf{true}$ and $\mathsf{false}$, too. – Dan Doel Jan 14 at 14:55
• I see. Thank you! – Samuel Jan 14 at 16:00