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

• An introduction to fibrations, topos theory, the effective topos and modest sets
• Scones, logical relations, parametricity