  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.
