The Axiom of Choice in Cartesian Bicategories

Authors Filippo Bonchi, Jens Seeber, Paweł Sobociński

Thumbnail PDF


  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Author Details

Filippo Bonchi
  • University of Pisa, Italy
Jens Seeber
  • IMT School for Advanced Studies Lucca, Italy
Paweł Sobociński
  • University of Southampton, UK

Cite AsGet BibTex

Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Logic
  • Cartesian bicategories
  • Axiom of choice
  • string diagrams


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77. Springer, 1967. Google Scholar
  2. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 710-719. ACM, 2016. Google Scholar
  3. Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski. Refinement for signal flow graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  4. Filippo Bonchi, Dusko Pavlovic, and Pawel Sobocinski. Functorial Semantics for Relational Theories. CoRR, abs/1711.08699, 2017. URL:
  5. Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:23, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL:
  6. Roberto Bruni and Fabio Gadducci. Some algebraic laws for spans (and their connections with multirelations). In Proc. RelMiS 2001, ENTCS, volume 44, 2001. Google Scholar
  7. Carsten Butz. Regular categories and regular logic. BRICS Lecture Series LS-98-2, 1998. Google Scholar
  8. Aurelio Carboni and Robert FC Walters. Cartesian bicategories I. Journal of pure and applied algebra, 49(1-2):11-32, 1987. Google Scholar
  9. Brandon Coya and Brendan Fong. Corelations are the prop for extraspecial commutative Frobenius monoids. Theory and Applications of Categories, 32(11):380-395, 2017. Google Scholar
  10. Brendan Fong. The Algebra of Open and Interconnected Systems. PhD thesis, University of Oxford, 2016. Google Scholar
  11. Brendan Fong and David I Spivak. Graphical Regular Logic. arXiv preprint arXiv:1812.05765, 2018. Google Scholar
  12. Brendan Fong and Fabio Zanasi. Universal Constructions for (Co)Relations: categories, monoidal categories, and props. Logical Methods in Computer Science, Volume 14, Issue 3, September 2018. URL:
  13. Thomas Fox. Coalgebras and cartesian categories. Communications in Algebra, 4(7):665-667, 1976. Google Scholar
  14. Peter J Freyd and Andre Scedrov. Categories, allegories, volume 39. Elsevier, 1990. Google Scholar
  15. Ichiro Hasuo and Naohiko Hoshino. Semantics of higher-order quantum computation via geometry of interaction. Annals of Pure and Applied Logic, 168(2):404-469, 2017. Google Scholar
  16. Horst Herrlich. Axiom of choice. Springer, 2006. Google Scholar
  17. Bart Jacobs. Categorical logic and type theory, volume 141. Elsevier, 1999. Google Scholar
  18. Bart Jacobs and Jorik Mandemaker. Coreflections in algebraic quantum logic. Foundations of physics, 42(7):932-958, 2012. Google Scholar
  19. Peter T Johnstone. Sketches of an elephant: A topos theory compendium, volume 2. Oxford University Press, 2002. Google Scholar
  20. Stephen Lack. Composing props. Theory and Applications of Categories, 13(9):147-163, 2004. Google Scholar
  21. Samuel J Mason. Feedback theory-some properties of signal flow graphs. Proceedings of the IRE, 41(9):1144-1156, 1953. Google Scholar
  22. E. Patterson. Knowledge Representation in Bicategories of Relations. ArXiv e-prints, June 2017. URL:
  23. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. Google Scholar
  24. Thomas Streicher. Semantics of type theory: correctness, completeness and independence results. Springer Science & Business Media, 2012. Google Scholar
  25. Fabio Zanasi. Interacting Hopf Algebras: the theory of linear systems. PhD thesis, Ecole Normale Supérieure de Lyon, 2015. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail