%0 Generic
%A Bonchi, Filippo
%A Di Giorgio, Alessandro
%A Trotta, Davide
%C Wadern, Germany
%D 2024
%E Královič, Rastislav
%E Kučera, Antonín
%F discovery:10198560
%I Dagstuhl Publishing
%K Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams
%P 30:1-30:19
%T When Lawvere Meets Peirce: An Equational  Presentation of Boolean Hyperdoctrines
%U https://discovery.ucl.ac.uk/id/eprint/10198560/
%V 306
%X Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere’s hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.
%Z Copyright © Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta;  licensed under Creative Commons License CC-BY 4.0, https://creativecommons.org/licenses/by/4.0/legalcode.