Formal P-Category Theory and Normalization by Evaluation in Rocq. - David G. Berry; Marcelo P. Fiore (CoRR, 2025)