A Universe of Sorts

take $C$ a category. There is a global sections functor $\Gamma: C -> Set$ given by $Hom(1, -)$ .
take the pullback $C \xrightarrow{\Gamma} Set \xleftarrow{cod} Set^{\to}$ .

From any type theory $T$ , we build $syn(T)$ , where objects are the types, and morphisms are terms with free variables. (ie, $A \to B$ is a term of type $B$ involving a free variable of type $A$ )
whatever structure $T$ had will be visible in $syn(T)$ . eg: if $T$ has products, then $syn(T)$ will have products. moreover, $syn(T)$ will be the initial such category. For any other $C$ with the appropriate structure, there will a functor $syn(T) \to C$ .
To use this to prove properties of $T$ , we'll need to cook up a special $C$ , so that $syn(T) \to C$ can tell us something. Further, this $C$ must somehow depend on $T$ to explore properties of $T$ , so let's call it $C(T)$ .
We must use the uniqueness of the morphism $syn(T)$ to $C(T)$ (ie, the initiality of $syn(T)$ ), because that's what makes this thing universal.

§ Scones