A Universe of Sorts

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

§ Presheaf Models of Type Theory