Maths - Contexts - Martin Baker

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.

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:

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

EuclideanSpace

home

Example - Database

Here we look at types of functions between sets in terms of a relational database. More information about databases on page here.

I think this gives a slightly different way to think about functions that

As a Presheaf Think about C^op as a database schema and the database tables as sets. This implements a category of simplical databases. More about this idea on page here.
One to Many Relational databases have many to one relationships between tables. For instance, if the database holds census data, then we may have: A table with an entry for each person. A table with an entry for each residence. There might then be a many to one relationship between these two tables. More information about relational databases on page here.
Many to Many In order to implement many to many relationships between tables we need to insert an extra table between them: This allows us to view a function as a set of pairs as in traditional set theory. See also pushout.
Pullback Reversing the functions so they go inward gives a structure like a pullback. See also pullback.

metadata block

see also:

http://www.mathreference.com/

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.

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.