Categories of partial equivalence relations as localizations

Abstract

We construct a category of fibrant objects $\mathbb{C}⟨P⟩$ in the sense of K. Brown from any indexed frame (a kind of indexed poset generalizing triposes) $P$, and show that its homotopy category is the Barr-exact category $\mathbb{C}[P]$ of partial equivalence relations and compatible functional relations. In particular this gives a presentation of realizability toposes as homotopy categories. We give criteria for the existence of left and right derived functors to functors $\mathbb{C}⟨\Phi ⟩:\mathbb{C}⟨P⟩\to \mathbb{C}⟨Q⟩$ induced by finite-meet-preserving transformations $\Phi :P\to Q$ between indexed frames.

26 pages