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