Hybrid dynamical systems exhibit a diverse array of stability phenomena, each currently addressed by separate Lyapunov-like results. We show that these results are all instances of a single theorem: a Lyapunov function is a morphism from a hybrid system into a simple stable target system $𝜎$, and different stability notions such as Lyapunov stability, asymptotic stability, exponential stability, and Zeno stability correspond to different choices of $𝜎$. This unification is achieved by expressing hybrid systems as coalgebras of an endofunctor $\mathrm{\mathscr{H}︀}$ on a category $\text{𝖢𝗁𝖺𝗋𝗍}$ that naturally blends continuous and discrete dynamics. Instantiating a general categorical Lyapunov theorem for coalgebras to this setting results in new Lypaunov-like conditions for the stability of Zeno equilibria and the existence of Zeno behavior in hybrid systems.

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

We give a characterization of colored Petri nets as monoidal double functors. Framing colored Petri nets in terms of category theory allows for canonical definitions of various well-known constructions on colored Petri nets. In particular, we show how morphisms of colored Petri nets may be understood as natural transformations. The displayed category construction explains how lax double functors are equivalent to functors with codomain their former domain. We use this result to characterize the unfolding of colored Petri nets in terms of free symmetric monoidal categories.

We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations – which axiomatise the usual notion of sets-with-relations – provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.

Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics.

Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV.

Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata’s $\top \top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.

We introduce contextads and the Ctx construction, unifying various structures and constructions in category theory dealing with context and contextful arrows – comonads and their Kleisli construction, actegories and their Para construction, adequate triples and their Span construction. Contextads are defined in terms of Lack–Street wreaths, suitably categorified for pseudomonads in a tricategory of spans in a 2-category with display maps. The associated wreath product provides the Ctx construction, and by its universal property we conclude trifunctoriality. This abstract approach lets us work up to structure, and thus swiftly prove that, under very mild assumptions, a contextad equipped colaxly with a 2-algebraic structure produces a similarly structured double category of contextful arrows. We also explore the role contextads might play qua dependently graded comonads in organizing contextful computation in functional programming. We show that many side-effects monads can be dually captured by dependently graded comonads, and gesture towards a general result on the ‘transposability’ of parametric right adjoint monads to dependently graded comonads.

We generalise an existing construction of Bayesian Lenses to admit lenses between pairs of objects where the backwards object is dependent on states on the forwards object (interpreted as probability distributions). This gives a natural setting for studying stochastic maps with Bayesian inverses restricted to the points supported by a given prior. In order to state this formally we develop a proposed definition by Fritz of a support object in a Markov category and show that these give rise to a section into the category of dependent Bayesian lenses encoding a more canonical notion of Bayesian inversion.

In this thesis, we present a flexible framework for specifying and constructing operads which are suited to reasoning about network construction. The data used to present these operads is called a network model, a monoidal variant of Joyal’s combinatorial species. The construction of the operad required that we develop a monoidal lift of the Grothendieck construction. We then demonstrate how concepts like priority and dependency can be represented in this framework. For the former, we generalize Green’s graph products of groups to the context of universal algebra. For the latter, we examine the emergence of monoidal fibrations from the presence of catalysts in Petri nets.

Petri networks and network models are two frameworks for the compositional design of systems of interacting entities. Here we show how to combine them using the concept of a ‘catalyst’: an entity that is neither destroyed nor created by any process it engages in. In a Petri net, a place is a catalyst if its in-degree equals its out-degree for every transition. We show how a Petri net with a chosen set of catalysts gives a network model. This network model maps any list of catalysts from the chosen set to the category whose morphisms are all the processes enabled by this list of catalysts. Applying the Grothendieck construction, we obtain a category fibered over the category whose objects are lists of catalysts. This category has as morphisms all processes enabled by some list of catalysts. While this category has a symmetric monoidal structure that describes doing processes in parallel, its fibers also have premonoidal structures that describe doing one process and then another while reusing the catalysts.

Networks can be combined in various ways, such as overlaying one on top of another or setting two side by side. We introduce “network models” to encode these ways of combining networks. Different network models describe different kinds of networks. We show that each network model gives rise to an operad, whose operations are ways of assembling a network of the given kind from smaller parts. Such operads, and their algebras, can serve as tools for designing networks. Technically, a network model is a lax symmetric monoidal functor from the free symmetric monoidal category on some set to $\text{𝐂𝐚𝐭}$, and the construction of the corresponding operad proceeds via a symmetric monoidal version of the Grothendieck construction.