Abstract Traditional category theory is typically based on set-theoretic principles and ideas, which are often nonconstructive. An alternative approach to formalizing category theory is to use e -category theory, where hom sets become setoids. Our work reconsiders a third approach – p -category theory – from Čubrić et al. (Mathematical Structures in Computer Science 8 (2) 153–192, 1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of p -category theory – where homs become subsetoids – and apply it to formalizing algorithms for normalization by evaluation, which are purely categorical but, surprisingly, do not use neutral and normal terms. Čubrić et al. (Mathematical Structures in Computer Science 8 (2) 153–192, 1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this, we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed -calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long) -normal forms of simply typed -terms together with a derivation of -conversion.
Berry et al. (Thu,) studied this question.