A note on “Extensional PERs”

Abstract

In the paper “Extensional PERs” by P. Freyd, P. Mulry, G. Rosolini and D. Scott, a category of “pointed complete extensional PERs” and computable maps is introduced to provide an instance of an 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 when 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.