Categories of partial equivalence relations as localizations

TL;DR

This paper constructs a category of fibrant objects from indexed frames, showing its homotopy category corresponds to partial equivalence relations, thus providing a new perspective on realizability toposes and derived functors.

Contribution

It introduces a method to build fibrant categories from indexed frames and relates their homotopy categories to partial equivalence relations, offering a new approach to realizability toposes.

Findings

Homotopy category of constructed fibrant objects is Barr-exact.

Provides criteria for existence of derived functors between these categories.

Shows realizability toposes as homotopy categories.

Abstract

We construct a category of fibrant objects $\mathbb{C}\langle P\rangle$ 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}\langle\Phi\rangle : \mathbb{C}\langle P\rangle\to \mathbb{C}\langle Q\rangle$ induced by finite-meet-preserving transformations ${\Phi} : P \to Q$ between indexed frames.