TY  - GEN
EP  - 30:19
SN  - 1868-8969
N2  - 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.
T3  - Leibniz International Proceedings in Informatics (LIPIcs)
Y1  - 2024/08/23/
N1  - 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.
TI  - When Lawvere Meets Peirce: An Equational
Presentation of Boolean Hyperdoctrines
AV  - public
CY  - Wadern, Germany
A1  - Bonchi, Filippo
A1  - Di Giorgio, Alessandro
A1  - Trotta, Davide
UR  - https://doi.org/10.4230/LIPIcs.MFCS.2024.30
KW  - Relational algebra; hyperdoctrines; cartesian bicategories; string diagrams
PB  - Dagstuhl Publishing
SP  - 30:1
ID  - discovery10198560
ER  -