Maths - Type Theory to Category Theory

We can relate type theory to category theory by linking:

So if a category has various objects each of these could be related to a type. type to category

Example of Set

How could a set type be related to a set category?

In the diagram below each object is a set of a given size.

This diagram doesn't yet reflect the nature of set since set category can have an arrow from every set to every other set except empty set. set example

In order to construct Nat or Vect above we need to call multiple constructors for each instance, for example, to constuct '2' we need to call Z and S and S. So is this a single instance of a type or 3 instances?

Category Theory, Logic and Type Theory

Category Theory Logic Type Theory
object say A, B ...   type
arrow say m:A->B relation
proved term
inhabited term
idA reflexitiviy  
given m:A->B and n:B->C there is n•m:A->C    
given e:E->A then idA•e=e
and given m:A->B then m•idA=m
given m:A->B and n:B->C and l:C->D then l•(n•m)=(l•n)•m    

Cartesian Closed Category (CCC)

In category theory the locally closed Cartesian category is the counterpart of extensional type theory.

For intensional type theory we need to add quotient completions - used for modeling extensional type theories into intensional ones.

see W-types

The category C is called Cartesian closed if and only if it satisfies the following three properties:

Examples specially relevant to type theory:

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.