# Type Theory via Exact Categories

### L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott.

**Abstract**

Partial equivalence relations (and categories of these) are a standard
tool in semantics of type theories and programming languages, since
they often provide a Cartesian closed category with extended
definability. Using the theory of exact categories, we give a
category-theoretic explanation of why the construction of a category
of partial equivalence relations often produces a Cartesian closed
category. We show how several familiar examples of categories of
partial equivalence relations fit into the general framework.
###
Table of Contents

**1. Introduction**
**2. Motivating Exact Categories**
**3. Defining Exact Categories**
**4. Application to PERs**
**5. On the Natural Numbers**
**6. Concluding Remarks**