Formal ᴘ‑Category Theory and Normalisation for Simple Type Theory

This thesis extends ᴘ‑category theory, introduced in Čubrić et al. (1998), and develops ᴘ‑bicategory theory, and thereafter uses them to conduct a ᴘ‑categorical analysis and synthesis of normalisation by evaluation for simple type theory. ᴘ‑category theory was introduced as a non-standard categorical framework for phrasing the normalisation by Yoneda embedding result of Čubrić et al. (1998). They provide only a minimal collection of definitions for their result and analysis. We extend their base theory into encompassing more definitions from standard category theory thereby demonstrating the robustness of their base theory as well as its utility in providing a non-standard framework for formalised category theory. Moreover, we augment ᴘ‑category theory into ᴘ‑bicategory theory, allowing the incorporation of bicategory theory into this non-standard framework. We use this ᴘ‑categorical framework to formalise the categorical and universal structure of simple type theory, allowing the reconstruction of the normalisation result of Čubrić et al. (1998). We broaden their result with a fuller analysis, allowing for alternative presentations thereof, and combine their techniques with a new universal property of unquotiented well-typed syntax of simple type theory. This allows for a fully-categorical proof of the basic correctness properties of normalisation by evaluation for simple type theory, without resorting to neutral and normal types, a proof not known to have been done before. Finally, we use our ᴘ‑categorical framework to formalise the normalisation result of Fiore (2002, 2022), to allow comparisons to be made with our work, and to demonstrate the strengths of ᴘ‑category theory for type-theoretic formalisation. All the normalisation results, and ᴘ‑categorical constructions required therefor have been formalised in the proof assistant Rocq.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2025

Author dc:creator

• Berry, David

Advisor dc:contributor.advisor

• Fiore, Marcelo

• ᴘ‑Category Theory
• Rocq
• Type Theory

Licence

• https://www.repository.cam.ac.uk/bitstreams/dbf09119-9dff-46e0-97f6-92e2a0f9e2ef/download
• http://purl.org/NET/rdflicense/allrightsreserved

Language dc:language

eng

DOI dc:identifier.doi

https://doi.org/10.17863/CAM.126527

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/397373