## § Presheaf models of type theory

- Let $C$ be any category.
- Contexts are presheaves $\Gamma: C^op \to Set$. Morphisms are natural transformations of presheaves.
- an element of a context $Elem(\Gamma)$ is a global element / grothendieck construction / object in the category of elements of contexts: $\Sigma{I:Ob(C)} \Gamma(I)$
- A type in the context, $\Gamma \vdash T$ is a presheaf over the category of elements $\alpha \in T(I, \rho)$.
- A term $\Gamma \vdash t: T$ is $t: (I: Ob(C)) -> (\rho: \Gamma(I)) -> T(I, \rho)$.
- substitution is a natural transformation $\sigma: \Gamma \to \Delta$.