Document Open Access Logo

Bicategories in Univalent Foundations

Authors Benedikt Ahrens , Dan Frumin , Marco Maggesi , Niels van der Weide

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.5.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • bicategory theory
  • univalent mathematics
  • dependent type theory
  • Coq

Metrics

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

Abstract

We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of "displayed bicategories", an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.

Cite As Get BibTex

Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.5

Author Details

Benedikt Ahrens
  • School of Computer Science, University of Birmingham, United Kingdom
Dan Frumin
  • Institute for Computation and Information Sciences, Radboud University, Nijmegen, The Netherlands
Marco Maggesi
  • Dipartimento di Matematica e Informatica "Dini", Università degli Studi di Firenze, Italy
Niels van der Weide
  • Institute for Computation and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

Work on this article was supported by a grant from the COST Action EUTypes CA15123.
  • Ahrens, Benedikt: This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-17-1-0363. Ahrens acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year.
  • Frumin, Dan: Supported by the Netherlands Organisation for Scientific Research (NWO/TTW) under the STW project 14319.
  • Maggesi, Marco: MIUR, GNSAGA-INdAM.

Acknowledgements

We would like to express our gratitude to all the EUTypes actors for their support. We also thank Niccolò Veltri for commenting on a draft of this paper. Finally, we thank the referees for their careful reading and thoughtful and constructive criticism.

References

  1. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 2015. URL: http://dx.doi.org/10.1017/S0960129514000486.
  2. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, 15(1), 2019. URL: http://dx.doi.org/10.23638/LMCS-15(1:20)2019.
  3. Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical structures for type theory in univalent foundations. Logical Methods in Computer Science, 14(3), September 2018. URL: http://dx.doi.org/10.23638/LMCS-14(3:18)2018.
  4. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2):241-286, 2018. URL: http://dx.doi.org/10.1017/S0960129516000268.
  5. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/BFb0074299.
  6. Robert Blackwell, Gregory M Kelly, and A John Power. Two-dimensional monad theory. Journal of Pure and Applied Algebra, 59(1):1-41, 1989. URL: http://dx.doi.org/10.1016/0022-4049(89)90160-6.
  7. Paolo Capriotti and Nicolai Kraus. Univalent higher categories via complete Semi-Segal types. PACMPL, 2(POPL):44:1-44:29, 2018. URL: http://dx.doi.org/10.1145/3158132.
  8. Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science, 24(6), 2014. URL: http://dx.doi.org/10.1017/S0960129513000881.
  9. Peter Dybjer. Internal Type Theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_66.
  10. Peter Dybjer and Hugo Moeneclaey. Finitary Higher Inductive Types in the Groupoid Model. Electr. Notes Theor. Comput. Sci., 336:119-134, 2018. URL: http://dx.doi.org/10.1016/j.entcs.2018.03.019.
  11. Eric Finster and Samuel Mimram. A type-theoretical definition of weak ω-categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005124.
  12. Marcelo Fiore. Discrete Generalised Polynomial Functors, 2012. Slides from talk given at ICALP 2012, URL: http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf.
  13. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83-111. Oxford Univ. Press, New York, 1998. Google Scholar
  14. Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky), 2012. URL: http://arxiv.org/abs/1211.2851.
  15. Ambroise Lafont, Tom Hirschowitz, and Nicolas Tabareau. Types are weak omega-groupoids, in Coq. Talk at TYPES 2018, URL: https://types2018.projj.eu/wp-content/uploads/2018/06/BookOfAbstractsTYPES2018.pdf.
  16. Tom Leinster. Basic Bicategories, 1998. URL: http://arxiv.org/abs/math/9810017.
  17. The Coq development team. http://coq.inria.fr, 2018. Version 8.8.
  18. nLab authors. Bicategory, December 2018. URL: http://ncatlab.org/nlab/revision/bicategory/43.
  19. Andrew M. Pitts. Categorical Logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, chapter 2, pages 39-128. Oxford University Press, 2000. Google Scholar
  20. Paul Taylor. Practical Foundations of Mathematics, volume 59 of Cambridge studies in advanced mathematics. Cambridge University Press, 1999. Google Scholar
  21. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  22. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. Available at URL: https://github.com/UniMath/UniMath.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact