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