On Doctrines and Cartesian Bicategories

TL;DR

This paper explores the connection between cartesian bicategories and elementary existential doctrines, establishing an adjunction and conditions for their equivalence, thus bridging algebraic and logical frameworks.

Contribution

It demonstrates an adjunction between cartesian bicategories and elementary existential doctrines, and identifies conditions for their categorical equivalence.

Findings

Established an adjunction between the two frameworks.

Identified conditions for their categorical equivalence.

Bridged algebraic and logical approaches to structural properties.

Abstract

We study the relationship between cartesian bicategories and a specialisation of Lawvere's hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.