Three studies in higher category theory: fibrations, skew monoidal structures and excision of extremals

Theoretical thesis.Bibliography: pages 159-162.1. Introduction -- 2. Fibred 2-categories and bicategories -- 3. The Catalan simplicial set -- 4. The Catalan simplicial set II -- 5. A formal verification of the theory of parity complexes.Many fundamental constructions from ordinary category theory can be generalised to higher categories. Obvious examples include adjunctions, monads, algebras, limits, and colimits. This thesis explores three cases where a construction from category theory is extended to higher categories.We first consider (Grothendieck) fibrations and the Grothendieck construction. We generalise fibrations to the contexts of 2-categories and bicategories. A fibration of bicategories exhibits many of the usual properties of ordinary fibrations. The main result is the Grothendieck construction which presents a correspondence between fibrations of bicategories and contravariant trihomomorphisms into the tricategory of bicategories.We next consider skew monoidal categories. Our goal is to uncover a definition of skew monoidal bicategory (a definition which is non-trivial due to the absence of a coherence theorem for skew monoidal categories). We do this by introducing the Catalan simplicial set C and show that simplicial maps from C into an appropriate nerve of Cat are precisely skew-monoidal categories. This simplicial set has a similar classifying property for skew monoidales internal to any monoidal bicategory. By examining simplicial maps from C to a suitable nerve of Bicat we obtain a definition of skew-monoidal bicategory that is consistent with existing definitions of monoidal bicategory.Finally, we consider Street's paper Parity Complexes. Parity complexes are multi-dimensional graph-like objects that exhibit the minimal structure required to build free n-categories such as the orientals. Due to its detailed combinatorial nature, the material in this paper can be difficult to follow and quite hard to verify. Indeed, there are minor errors in the original text that were later corrected. We present a formalisation, in Coq, of this theory up to the excision of extremals algorithm in Section 4. We have verified that Street's work is fundamentally sound and that there are no further errors. We summarise the main content of the theory, and the basic intuition involved in its construction. We also discuss some technical aspects of the formalisation, and comment on which portions of the theory could benefit from some refinement.Mode of access: World wide web1 online resource (x, 162 pages