Formal P-Category Theory and Normalization by Evaluation in Rocq

David G. Berry, Marcelo P. Fiore

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to…