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: Cop -> Set.
|Morphisms between sheaves represent substitutions.
More about contexts on page here.
∫ P is a set of pairs where: