Uniform Monad Presentations and Graph Quasitoposes

Category theory is a field of mathematics that provides a unifying framework for the generalisation of mathematical definitions and theorems, and which has found significant applications in computer science. This thesis explores two such applications: uniform algebraic presentations of monads and quasitoposes in graph rewriting.

Part I of this thesis studies monads, which serve as a unifying framework for modelling computational effects in programming languages. A key aspect of monads is their correspondence with algebraic theories, where an algebraic theory that corresponds to a monad is called an algebraic presentation of that monad. Composing monads allows to combine their computational effects and is often performed via distributive laws, which correspond to the algebraic notion of composite theories. This thesis provides a complete and constructive proof of this correspondence and establishes criteria that ensure a certain minimal set of distributivity equations suffices to axiomatise the composite theory. To achieve this, we employ term rewriting techniques and introducing functor rewriting systems. Important results in the literature rely on the correspondence we proved, namely no-go theorems, which establish that certain distributive laws cannot exist. The non-existence of certain distributive laws has motivated investigations into weaker notions of distributive laws, called weak distributive laws. In this context, semifree monads were introduced to establish a correspondence between distributive laws for a given monad and weak distributive laws for its semifree monad. The second main contribution of Part I proves how an algebraic presentation of a monad can be systematically transformed into a presentation of its semifree monad.

Part II of this thesis studies quasitoposes and their role in graph rewriting, a rule-based framework for transforming graphs. The diversity of graph definitions makes it impractical to develop a separate rewriting formalism for each type. Category theory offers a unified approach for defining formalisms in a graph-agnostic manner. Moreover, quasitoposes, which are categories with spe285 286 Summary cific properties, have emerged as a promising framework for comparing rewriting formalisms, studying meta-theorems for non-linear rewriting, facilitating relabelling, and supporting categorical termination methods. This thesis develops two methods for identifying new quasitoposes: one via fuzzy presheaves and the other via Lawvere-Tierney (LT) topologies. Fuzzy presheaves are introduced as a generalisation of fuzzy sets and fuzzy graphs, and their categories are shown to be rm-adhesive quasitoposes. The second approach provides a complete characterisation of LT-topologies and of their separated elements and sheaves in the categories of simplicial sets, bicoloured graphs, fuzzy sets, and fuzzy graphs, leading to the identification of new quasitoposes.