Regular Functors and Relative Realizability Categories

TL;DR

This paper introduces a universal property-based framework for defining and constructing relative realizability categories over arbitrary Heyting bases, expanding the understanding of geometric morphisms to these toposes.

Contribution

It generalizes the concept of relative realizability categories beyond the set-based case using a universal property approach.

Findings

Provides a construction method for relative realizability categories over any Heyting category.

Identifies new geometric morphisms to relative realizability toposes.

Extends the theoretical foundation of realizability toposes.

Abstract

Relative realizability toposes satisfy a universal property that involves regular functors to other categories. We use this universal property to define what relative realizability categories are, when based on other categories than of the topos of sets. This paper explains the property and gives a construction for relative realizability categories that works for arbitrary base Heyting categories. The universal property shows us some new geometric morphisms to relative realizability toposes too.