From the 1 of 4 linked papers with an AI index.
4 papers
Bidirectional Elaborators à la Carte
Andrew Slattery, Jonathan Sterling
The paper presents a dependently‑typed monadic DSL for specifying elaboration algorithms in proof assistants, using a shallow embedding of a bidirectional surface language for Mart…
Hofmann-Streicher lifting of fibred categories
Andrew Slattery, Jonathan Sterling
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 c…
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…
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…