TY  - RPRT
TI  - Formal P-Category Theory and Normalization by Evaluation in Rocq
AU  - David G. Berry
AU  - Marcelo P. Fiore
PY  - 2025
UR  - https://arxiv.org/abs/2505.07780
ID  - 2505.07780
ER  -