When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines
<|reference_start|>When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines: 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.<|reference_end|>
@article{bonchi2024when,
    title={When Lawvere meets Peirce: an equational presentation of boolean
  hyperdoctrines},
    author={Filippo Bonchi, Alessandro Di Giorgio, Davide Trotta},
    journal={arXiv preprint arXiv:2404.18795},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.18795},
    primaryClass={math.CT cs.LO}
}