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.