Primitive recursion, equality, and a universal set
Michael Pfender, M. Kröplin, D. Pape · Mathematical Structures in Computer Science · 1994
Within a categorical framework for primitive recursion, equality between p.r. maps is shown to be definable by suitable p.r. equality predicates. Equivalence is shown between a direct categorical formalization of classical p.r. functions and p.r. maps in the sense of Lawvere and Freyd. An extension of the theory is shown to admit a ‘universal set’ containing all objects of the extended theory of subobjects.