§ Presheaf models of type theory
- Let be any category.
- Contexts are presheaves . Morphisms are natural transformations of presheaves.
- an element of a context is a global element / grothendieck construction / object in the category of elements of contexts:
- A type in the context, is a presheaf over the category of elements .
- A term is .
- substitution is a natural transformation .