arXiv subjects

Andrew Slattery

Publications and source records attributed to Andrew Slattery.

5 recordsLinked to original sources

arXiv2026

Bidirectional Elaborators \`a la Carte

Surface syntax in proof assistants like Rocq, Lean, Agda, and Idris is highly implicit, lacking many details that are needed for user-written code to denote precisely defined mathematical objects. Elaboration is an algorithm that accounts for these details by translating surface syntax to an explicit enough core syntax. The reliability and predictability of elaboration relies on several critical properties of the core type system, including decidability of judgemental equality and the injectivity of type constructors; these dependencies are witnessed in a concrete system by explicit calls to conversion checking and weak-head reduction subroutines. We introduce a dependently typed monadic domain specific language for the executable specification of correct-by-construction elaboration algorithms that is abstracted from any particular representation of normal forms or algorithm for conversion checking. In particular, we represent a bidirectionally typed surface language for Martin-L\"of type theory by shallow embedding in this DSL so that the translation of surface terms into core terms amounts to elementary equational calculation. This translation is correct by construction in the sense that it cannot produce ill-typed terms, and is automatically stable under judgemental equality of core terms and even under substitution; from the latter property, we obtain a new denotational interpretation of the suspension of elaboration problems. Finally, a concrete elaboration algorithm is extracted by algebraic means from a presheaf model of the DSL built out of the bi-initial natural model of Martin-L\"of type theory.

cs.PL↗

arXiv2025

Idempotence for relative monads

We study the concept of idempotence for relative monads, which exhibits several subtleties not present for non-relative monads. In particular, there is a bifurcation of notions of idempotence in the relative setting, which are indistinguishable for idempotent monads. As a special case, we obtain several characterisations of idempotence for monads in extension form.

math.CT↗

arXiv2025

Hofmann-Streicher lifting of fibred categories

In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe from the category of sets into the category of set-valued presheaves on a small category. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the categorical nerve, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, the categorical nerve's functorial action on the universal small discrete fibration gives the generic family of the universe's Hofmann-Streicher lifting. Inspired by Awodey's analysis, we define a relative version of Hofmann-Streicher lifting in terms of the right pseudo-adjoint to the 2-functor given by postcomposition with a fibration. Finally, we construct a new 2-bifibration of fibrations in which the opcartesian and cartesian lifts arise from these pseudo-adjunctions.

math.CT↗

arXiv2025

Bicategories of algebras for relative pseudomonads

We introduce pseudoalgebras for relative pseudomonads and develop their theory. For each relative pseudomonad $T$, we construct a free--forgetful relative pseudoadjunction that exhibits the bicategory of $T$-pseudoalgebras as terminal among resolutions of $T$. The Kleisli bicategory for $T$ thus embeds into the bicategory of pseudoalgebras as the sub-bicategory of free pseudoalgebras. We consequently obtain a coherence theorem that implies, for instance, that the bicategory of distributors is biequivalent to the 2-category of presheaf categories. In doing so, we extend several aspects of the theory of pseudomonads to relative pseudomonads, including doctrinal adjunction, transport of structure, and lax-idempotence. As an application of our general theory, we prove that, for each class of colimits $\Phi$, there is a correspondence between monads relative to free $\Phi$-cocompletions, and $\Phi$-cocontinuous monads on free $\Phi$-cocompletions.

math.CT↗

arXiv2023

Pseudocommutativity and Lax Idempotency for Relative Pseudomonads

We extend the classical work of Kock on strong and commutative monads, as well as the work of Hyland and Power for 2-monads, in order to define strong and pseudocommutative relative pseudomonads. In order to achieve this, we work in the more general setting of 2-multicategories rather than monoidal 2-categories. We prove analogous implications to the classical work: that a strong relative pseudomonad is a pseudo-multifunctor, and that a pseudocommutative relative pseudomonad is a multicategorical pseudomonad. Furthermore, we extend the work of L\'opez Franco with a proof that a lax-idempotent strong relative pseudomonad is pseudocommutative. We apply the results of this paper to the example of the presheaf relative pseudomonad.

math.CT↗