Uploaded September 2025 | Updated September 2026, 2 weeks ago

---

Topos Institute Colloquium, 11th of September 2025.
———
Many of the classical tools of categorical algebra can be generalized
to the world of higher algebra, that is, the study of algebraic
structures on homotopy types. Indeed we can talk about ∞-Lawvere
theories, ∞-finite limit theories, classifying ∞-topoi, ∞-operads and
so on. That we can define and reason about such higher algebraic
theories is a result of the well-developed theory of (∞,1)-categories
of Joyal and Lurie, and ultimately relies on the tractability of
working combinatorially with simplices.

Type theorists and computer scientists often work with presentations
of algebraic theories using dependent types, so-called "Generalized
Algebraic Theories", exactly because they have convenient syntactic
descriptions which lend themselves to computer implementation. We can
generalize the categorical semantics of these theories to the higher
setting using the tools above, but doing so renders the connection to
concrete syntax somewhat tenuous.

In this talk I'll introduce a method for recovering a more syntactic
description of the notion of higher generalized algebraic theory by
introducing the category of dependetopes. The name derives from the
fact that the dependetopes can be understood as a dependently typed
extension of Baez-Dolan's notion of opetope which captures the higher
geometry of type-dependency. In addition to their definition, I will
explain how the dependetopes come with a concrete syntax arising from
type theory, which can be used to define and manipulate them.