The Categorial Semantics of Type Theory

In mathematical logic, A deductive system consists of

A type theory is a deductive system with two kinds of judgments:

We read \(x : A\) as \(x\) has type \(A\). The rules of inference vary greatly from type theory to type theory. Examples include:

\[\frac{}{x : A \vdash x : A} \qquad \frac{x : A \vdash f(x) : B \quad y : B \vdash g(y) : C}{x : A \vdash g(f(x)) : C} \]

I am interested in type theories because they can be used to design functional programming languages and they often have transparent categorial semantic models. A category has objects and morphism sets.

A good introduction to these ideas is the homotopy type theory book