Contexts in Type Theory
Contexts come from logic and are used in type theory to hold information about variables. C is a category of contexts and the individual contexts are denoted by upper case Greek letters: Γ,Δ… 1 is empty context. 

The structure of contexts is a sheaf: C^{op} > Set.  
Morphisms between sheaves represent substitutions. 
More about contexts on page here.
∫ P is a set of pairs where:
