Maths - Types - Contexts

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.

diagram category of contexts
The structure of contexts is a sheaf: Cop -> Set. diagram context sheaf
Morphisms between sheaves represent substitutions. diagram substitution

More about contexts on page here.

∫ P is a set of pairs where:

  • The first element is a context such as Γ
  • The second element is a variable in that context.













































metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.