3 papers
cs.PL2026
Bidirectional Elaborators à la Carte
Andrew Slattery, Jonathan Sterling
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 mathe…
math.CT2025
Idempotence for relative monads
Nathanael Arkor, Andrew Slattery
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…
math.CT2025
Bicategories of algebras for relative pseudomonads
Nathanael Arkor, Philip Saville, Andrew Slattery
We introduce pseudoalgebras for relative pseudomonads and develop their theory. For each relative pseudomonad , we construct a free--forgetful relative pseudoadjunction that exh…