PhD Thesis

A Generalized Algebraic Theory of Directed Equality


University of Nottingham, School of Computer Science
— Submitted: 05 June 2025
— Defended: 16 September 2025 [slides]
Visit the website: jacobneu.phd

Abstract. We develop a directed type theory capable of synthetic reasoning about 1-categories, with straightforward semantics in the category of categories. All our semantic notions are defined as generalized algebraic theories, permitting modular reasoning about different type theories and ensuring the existence of initial syntax models.

We define the category model of type theory—the directed analogue of Hofmann and Steicher's groupoid model—where contexts are interpreted as categories and types as (split opfibrant) displayed categories. Adapting the groupoid model semantics of key type formers, (dependent) functions and identity types in particular, requires us to adopt a modal typing discipline to track the variances of terms. We define a succession of model notions—polarized categories with families, neutral-polarized categories with families, and directed categories with families—to abstractly capture more and more of the type theory of the category model; this includes an axiomatization of how the groupoid model's undirected type theory is situated inside the category model's directed type theory.

The symmetric (i.e. invertible) identity types of the groupoid model become directed hom-types of the category model; we can show by metatheoretic argument that our polarized typing discipline prevents invertibility of hom-types from being provable in our directed type theory. Each type therefore has the structure of a synthetic category and each function a synthetic functor; this is all proved within the theory using the eliminator for hom-types, directed path induction. We expound a new style of categorytheoretic reasoning appropriate to this setting, where the universal mapping properties of standard category theory are all phrased as principles of induction.

To support these developments, we outline generalized algebra, the mathematical discipline concerned with generalized algebraic theories. In particular, we highlight the construction of an initial algebra for every GAT (which is what guarantees a syntax model for the notions of model we use) and the fact that every GAT gives rise to a "concrete category with families", a model of type theory whose contexts are algebras and types are displayed algebras. The groupoid and category models can be viewed as a modification of the concrete CwFs of groupoids and categories, respectively, which ensures the fibrancy of their types.

Current Work

Publications

Preprints

Talks


Master's Thesis

J. Neumann. Semantics of Nondeterministic Construction. Master's thesis, Carnegie Mellon University, 2020.
Slides from thesis defense

My master's thesis combines insights from modal logic, formal epistemology, and theoretical computer science into a mathematically-ambitious analysis of a very simple activity: flipping a coin. Based on an insight by my thesis advisor, Adam Bjorndahl, I develop dynamic topological logic as a suitable language for formally articulating and reasoning about the capacities of knowledgeable agents in situations where nondeterministic actions are possible. I focus on situations where our agent is able to flip a coin to choose between two possible courses of action, and rigorously examine how the uncertainty created by the coin interacts with the agent's capacity for knowledge.

This work is primarily focused on the model theory of dynamic topological logic: "equipping the agent with a coin to flip" corresponds mathematically to a kind of transformation of dynamic topological structures, which I call a program constructor. To fully elucidate the theory of program constructors requires extensive mathematical development, including the introduction of several novel notions in the theory of dynamic topological models and frames. Along the way, I develop a deep connection between program construction in the dynamic topological setting, and analogous processes in the relational model theory of propositional dynamic logic. Though this thesis leaves much work to be done, it establishes a robust framework for future exploration of this very rich topic.