PBPO+: A Unifiying Theory for Quasitoposes

Abstract

Last year we proposed PBPO+, which extends the Pullback-Pushout (PBPO) approach by Corradini et al. with strong matching. Now, we have proved that in the setting of quasitoposes (and assuming regular monic matching), PBPO+ can define all rewrite relations definable by PBPO, AGREE, SqPO and DPO – as well as additional ones. In this sense, PBPO+ can be considered a unifying theory in this setting. In this talk we reflect on the notion of a quasitopos, and explain how from its many nice properties our result can be obtained. This is joint work with Jörg Endrullis and Aloïs Rosset.