## § Scones

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