We can relate type theory to category theory by linking:
- types to objects
- terms to arrows
|So if a category has various objects each of these could be related to a type.
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.
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
|object say A, B ...
|arrow say m:A->B
|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.
The category C is called Cartesian closed if and only if it satisfies the following three properties:
- It has a terminal object.
- Any two objects X and Y of C have a product X ×Y in C.
- Any two objects Y and Z of C have an exponential ZY in C.
Examples specially relevant to type theory:
- In order theory, complete partial orders (cpos) have a natural topology, the Scott topology, whose continuous maps do form a Cartesian closed category (that is, the objects are the cpos, and the morphisms are the Scott continuous maps).
- A Heyting algebra is a Cartesian closed (bounded) lattice. An important example arises from topological spaces. If X is a topological space, then the open sets in X form the objects of a category O(X) for which there is a unique morphism from U to V if U is a subset of V and no morphism otherwise. This poset is a Cartesian closed category: the "product" of U and V is the intersection of U and V and the exponential UV is the interior of U∪(X\V).
- The category of simplicial sets (which are functors X : Δop -> Set) is Cartesian closed.