Type Theory via Exact Categories

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


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