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.
Please note that the meeting will be recorded and live-streamed to YouTube: