Suppose we have a dependent type theory which has dependent product types, dependent sum types, identity types, function extensionality, an empty type, and a universe $U$ which is closed under the above types. Already, we could construct a significant number of other types:
- Function types $A \to B$ are dependent product types for which the type family codomain is a constant type family
- Similarly, product types $A \times B$ are dependent sum types for which the type family codomain is a constant type family
- Equivalence types $A \simeq B$ are defined as usual in dependent type theory – from bi-invertible functions, functions with contractible fibers, etc…
- Pullbacks for functions $f:A \to C$ and $g:B \to C$ are given by the type $\sum_{a:A} \sum_{b:B} f(a) =_C g(b)$
- The unit type is given by the type of endofunctions on the empty type $\mathbb{1} \equiv \emptyset \to \emptyset$
- The type of propositions is given by the type $\mathrm{Prop} \equiv \sum_{A:U} \prod_{x:A} \prod_{y:A} x =_A y$, although it is large relative to $U$.
- Power sets are given by functions into $\mathrm{Prop}$, and are large relative to $U$
- Propositional truncations of a type $A$ are given by the type $[A] \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to P$, and are large relative to $U$
- The predicate logic operations: false $\bot \equiv [\emptyset]$, true $\top \equiv [\mathbb{1}]$, conjunction $A \wedge B \equiv [A \times B]$, implication $A \implies B \equiv [A \to B]$, negation $\neg A \equiv [A \to \emptyset]$, logical equivalence $A \iff B \equiv [A \simeq B]$, existential quantification $\exists x:A.B(x) \equiv \left[\sum_{x:A} B(x)\right]$, and universal quantification $\forall x:A.B(x) \equiv \left[\prod_{x:A} B(x)\right]$, which are all large relative to $U$
- Quotient sets: An equivalence relation is a function $R:A \times A \to \mathrm{Prop}$ which comes with dependent functions $r:\prod_{x:A} R(x, x)$, $s:\prod_{x:A} \prod_{y:A} R(x, y) \to R(y, x)$, and $t:\prod_{x:A} \prod_{y:A} \prod_{z:A} R(x, y) \times R(y, z) \to R(x, z)$. Given an equivalence relation $R:A \times A \to \mathrm{Prop}$, the quotient set $A/R$ is given by the type
$$A/R \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.R(x, y) \iff P(x)$$
and is large relative to $U$
One thing that is missing here are coproduct types and the booleans. In classical mathematics, where one has the double negation law for small propositions $\prod_{P:\mathrm{Prop}} \neg \neg P \to P$, the booleans type is the type of propositions $\mathrm{bool} \equiv \mathrm{Prop}$, and the coproduct types are then formed by the dependent sum type of a type family indexed by the type of propositions. However, in constructive mathematics, the booleans are only the decidable propositions – but we cannot define whether a proposition is decidable or not, because without coproduct types we cannot define disjunctions, which are used in the definition of a decidable proposition. Is there an alternate way of constructing either coproduct types or the booleans directly from the universe/type of propositions? No requirements are made of the size of the resulting coproduct types and booleans, they could be $U$-large if necessary.
Best Answer
I'll expand on Simon Henry's comment to a full answer.
We first define the disjunction of two types. Recall that traditionally, the disjunction of $A$ and $B$ is defined as the propositional truncation of the coproduct of $A$ and $B$: $$A \vee B \equiv [A + B].$$ Using the impredicative definition of propositional truncation above, we then have $$A \vee B \equiv \prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P.$$
For all types $A$, $B$, and $C$, there is an equivalence $$((A + B) \to C) \simeq ((A \to C) \times (B \to C))$$ and if $A \simeq B$, then $(A \to C) \simeq (B \to C)$. In addition, for all type families $x:A \vdash B(x)$, and $x:A \vdash C(x)$, if there is a family of equivalences $e:\prod_{x:A} B(x) \simeq C(x)$, then there is an equivalence $\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} C(x)\right)$. All this taken together means that there is an equivalence $$\left(\prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} ((A \to P) \times (B \to P)) \to P\right).$$ Uncurrying $((A \to P) \times (B \to P)) \to P$ in the above expression leads to Simon Henry's equivalent definition of the disjunction of two types.
$$A \vee B \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to (B \to P) \to P$$
From there it is easy to define the booleans as the type
$$\mathrm{bool} \equiv \sum_{P:\mathrm{Prop}} P \vee \neg P$$
and the coproduct types as
$$A + B \equiv \sum_{x:\mathrm{bool}} C(x)$$
where $C(\bot) \equiv A$ and $C(\top) \equiv B$.
On a side note, the same logic could be used to define the existential quantifier without using dependent sum types. We have the equivalence
$$\left(\prod_{P:\mathrm{Prop}} \left(\left(\sum_{x:A} B(x)\right) \to P\right) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P\right).$$ Thus, we could define $$\exists x:A.B(x) \equiv \prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P.$$
In a similar way, we can also define the empty type from the type of propositions. The empty type is a proposition, and thus is equivalent to its propositional truncation. By recursion on the empty type, every function type from the empty type is contractible and equivalent to the unit type. Now, every function type from a contractible type is equivalent to the codomain of the function type; thus, we have the following equivalences
$$\emptyset \simeq \left(\prod_{P:\mathrm{Prop}} (\emptyset \to P) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} \mathbb{1} \to P\right) \simeq \prod_{P:\mathrm{Prop}} P$$
and we could define
$$\emptyset \equiv \prod_{P:\mathrm{Prop}} P.$$
The resulting empty type is $U$-large.
The key thing here is that since each $P$ is a prop, by weak function extensionality, the type $\prod_{P:\mathrm{Prop}} P$ is also a proposition. If the type $\prod_{P:\mathrm{Prop}} P$ has an element, then every proposition has an element and is thus contractible, which implies that the universe $U$ itself is contractible and thus trivial. But we do not know if $\prod_{P:\mathrm{Prop}} P$ has an element, so $\prod_{P:\mathrm{Prop}} P$ behaves as the empty type.