Formal p -category theory and normalization by evaluation in Rocq

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 $\lambda$ -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) $\beta$ $\eta$ -normal forms of simply typed $\lambda$ -terms together with a derivation of $\beta$ $\eta$ -conversion.