{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/397373"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/397373","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Formal ᴘ‑Category Theory and Normalisation for Simple Type Theory","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Berry, David"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Fiore, Marcelo"],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-10-08","date_published":"2025-10-08","updated_at":"2026-07-22T22:24:27Z","subjects":["ᴘ‑Category Theory","Rocq","Type Theory"],"languages":["eng"],"rights":[],"rights_urls":["https://www.repository.cam.ac.uk/bitstreams/dbf09119-9dff-46e0-97f6-92e2a0f9e2ef/download","http://purl.org/NET/rdflicense/allrightsreserved"],"identifier_entries":[]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.126527","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Fiore, Marcelo"]},{"key":"dc:creator","label":"Author","values":["Berry, David"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2025-10-08"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/397373"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["ᴘ‑Category Theory","Rocq","Type Theory"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["https://www.repository.cam.ac.uk/bitstreams/dbf09119-9dff-46e0-97f6-92e2a0f9e2ef/download","http://purl.org/NET/rdflicense/allrightsreserved"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.17863/CAM.126527"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://www.repository.cam.ac.uk/bitstreams/eaa64944-8cd5-4cc3-8ff1-028e9b5a1cac/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["a343e50703ffa3e5d659dbd66796f91c","87eda9de84448d1f82354d60eee3eb5f"]},{"key":"dc:title","label":"Title","values":["Formal ᴘ‑Category Theory and Normalisation for Simple Type Theory"]}]}],"canonical_facts":{"dc:contributor.advisor":["Fiore, Marcelo"],"dc:creator":["Berry, David"],"dc:date.issued":["2025-10-08"],"dc:description.abstract":["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."],"dc:format.checksum.md5":["a343e50703ffa3e5d659dbd66796f91c","87eda9de84448d1f82354d60eee3eb5f"],"dc:identifier.doi":["https://doi.org/10.17863/CAM.126527"],"dc:identifier.uri":["https://www.repository.cam.ac.uk/bitstreams/eaa64944-8cd5-4cc3-8ff1-028e9b5a1cac/download"],"dc:language":["eng"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/397373"],"dc:rights":["https://www.repository.cam.ac.uk/bitstreams/dbf09119-9dff-46e0-97f6-92e2a0f9e2ef/download","http://purl.org/NET/rdflicense/allrightsreserved"],"dc:subject":["ᴘ‑Category Theory","Rocq","Type Theory"],"dc:title":["Formal ᴘ‑Category Theory and Normalisation for Simple Type Theory"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:24:27Z"}