The contribution of this thesis is a novel framework for rewriting in higher categories. Its theoretical foundation is the theory of quasistrict higher categories and the practical realisation is a proof assistant Globular. The framework introduces the notions of diagrams and signatures as new mutually-recursive structures that give the algebraic basis for the approach. These structures are related the notion of an n-polygraph, but allow reasoning about quasistrict higher categorical structures in a way amenable to computer implementation. Building on this, we propose a new definition of a quasistrict 4-category, and prove a result that in a quasistrict 4-category, an adjunction of 1-morphisms gives rise to a coherent adjunction satisfying the butterfly equations.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:740809 |
| Date | January 2016 |
| Creators | Bar, Krzysztof |
| Contributors | Abramsky, Samson ; Coecke, Bob |
| Publisher | University of Oxford |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://ora.ox.ac.uk/objects/uuid:ba1d3341-873d-4255-8400-c2277b7648f3 |
Page generated in 0.002 seconds