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

• A presheaf model of dependent type theory by Alexis Laouar
• Ref: Cubical type theory with several universes in nuprl