2 papers
cs.LO2025
Substructural Abstract Syntax with Variable Binding and Single-Variable Substitution
Marcelo Fiore, Sanjiv Ranchod
We develop a unified categorical theory of substructural abstract syntax with variable binding and single-variable (capture-avoiding) substitution. This is done for the gamut of co…
math.CT2024
A finite algebraic presentation of Lawvere theories in the object-classifier topos
Marcelo Fiore, Sanjiv Ranchod
Over the topos of sets, the notion of Lawvere theory is infinite countably-sorted algebraic but not one-sorted algebraic. Shifting viewpoint over the object-classifier topos, a fin…