A generalized algebraic theory of directed equality
Publication Date
July 31, 2026
Creator
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, which permit modular reasoning about different type theories and ensure 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 category- theoretic 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, that ensures the fibrancy of their types.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
82903
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
main.pdf
Type
Full-text
Description
Examined
Size
1.66 MB
Format
Adobe PDF
Checksum (MD5)
f7037eecf3c81d7f4131871b0166b1ae