A Note on "Extensional PERs"

TL;DR

This paper extends the concept of algebraic compactness to a category of pointed complete extensional PERs within the effective topos, enabling solutions to recursive equations for a broader class of functors.

Contribution

It generalizes the algebraic compactness property to include all internal functors on the category of pointed complete extensional PERs in the effective topos.

Findings

Category of pointed complete extensional PERs is algebraically compact.

Extension of algebraic compactness to all internal functors in the effective topos.

Provides foundational results for recursive equations in this categorical setting.

Abstract

In the paper "Extensional PERs" by P. Freyd, P. Mulry, G. Rosolini and D. Scott, a category $\mathcal{C}$ of "pointed complete extensional PERs" and computable maps is introduced to provide an instance of an \emph{algebraically compact category} relative to a restricted class of functors. Algebraic compactness is a synthetic condition on a category which ensures solutions of recursive equations involving endofunctors of the category. We extend that result to include all internal functors on $\mathcal{C}$ when $\mathcal{C}$ is viewed as a full internal category of the effective topos. This is done using two general results: one about internal functors in general, and one about internal functors in the effective topos.