Document Open Access Logo

Univalent Enriched Categories and the Enriched Rezk Completion

Author Niels van der Weide

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2024.4.pdf
  • Filesize: 0.87 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • enriched categories
  • univalent categories
  • homotopy type theory
  • univalent foundations
  • Rezk completion

Metrics

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

Abstract

Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.

Cite As Get BibTex

Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSCD.2024.4

Author Details

Niels van der Weide
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

  • van der Weide, Niels: This research was supported by the NWO project "The Power of Equality" OCENW.M20.380, which is financed by the Dutch Research Council (NWO).

Acknowledgements

The author thanks the anonymous reviewers of HoTT/UF and FSCD for their useful comments, Nima Rasekh for useful discussions, and Dan Frumin and Kobe Wullaert for proof reading earlier versions of this paper. The author also thanks the Coq developers for providing the Coq proof assistant and their continuous support to keep https://github.com/UniMath/UniMath compatible with Coq.

Supplementary Materials

References

  1. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Mathematical Structures in Computer Science, pages 1-38, 2022. URL: https://doi.org/10.1017/S0960129522000032.
  2. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010-1039, 2015. URL: https://doi.org/10.1017/S0960129514000486.
  3. Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert. Displayed monoidal categories for the semantics of linear logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 260-273. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636956.
  4. Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The univalence principle. CoRR, abs/2102.06275, 2021. URL: https://arxiv.org/abs/2102.06275.
  5. Alexander Campbell. Skew-enriched categories. Appl. Categ. Structures, 26(3):597-615, 2018. URL: https://doi.org/10.1007/s10485-017-9504-0.
  6. Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Román. Profunctor Optics, a Categorical Update. Compositionality, 6:1, February 2024. URL: https://doi.org/10.32408/compositionality-6-1.
  7. Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. The enriched effect calculus: syntax and semantics. J. Log. Comput., 24(3):615-654, 2014. URL: https://doi.org/10.1093/logcom/exs025.
  8. David Gepner and Rune Haugseng. Enriched ∞-categories via non-symmetric ∞-operads. Adv. Math., 279:575-716, 2015. URL: https://doi.org/10.1016/j.aim.2015.02.007.
  9. Paul G. Goerss and John F. Jardine. Simplicial homotopy theory. Modern Birkhäuser Classics. Birkhäuser Verlag, Basel, 2009. Reprint of the 1999 edition. URL: https://doi.org/10.1007/978-3-0346-0189-4.
  10. Jason Z. S. Hu and Jacques Carette. Formalizing category theory in Agda. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 327-342. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439922.
  11. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/JEMS/1050.
  12. Max Kelly. Basic concepts of enriched category theory, volume 64. CUP Archive, 1982. Google Scholar
  13. Stephen Lack and Ross Street. The formal theory of monads. II. J. Pure Appl. Algebra, 175(1-3):243-265, 2002. Special volume celebrating the 70th birthday of Professor Max Kelly. URL: https://doi.org/10.1016/S0022-4049(02)00137-8.
  14. Tom Leinster. A survey of definitions of n-category. Theory Appl. Categ., 10:1-70, 2002. Google Scholar
  15. Fosco Loregian and Emily Riehl. Categorical notions of fibration. Expo. Math., 38(4):496-514, 2020. URL: https://doi.org/10.1016/j.exmath.2019.02.004.
  16. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  17. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in proof theory. Bibliopolis, 1984. Google Scholar
  18. The mathlib Community. The Lean mathematical library. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  19. Dylan McDermott and Alan Mycroft. Galois connecting call-by-value and call-by-name. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 32:1-32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.FSCD.2022.32.
  20. Dylan McDermott and Tarmo Uustalu. What makes a strong monad? In Jeremy Gibbons and Max S. New, editors, Proceedings Ninth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022, volume 360 of EPTCS, pages 113-133, 2022. URL: https://doi.org/10.4204/EPTCS.360.6.
  21. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 14-23. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39155.
  22. Ulf Norell. Dependently typed programming in Agda. In Proceedings of the 4th international workshop on Types in language design and implementation, pages 1-2, 2009. Google Scholar
  23. Gordon Plotkin and John Power. Notions of computation determine monads. In International Conference on Foundations of Software Science and Computation Structures, pages 342-356. Springer, 2002. Google Scholar
  24. Gordon Plotkin and John Power. Algebraic operations and generic effects. Applied categorical structures, 11(1):69-94, 2003. Google Scholar
  25. John Power. Models for the computational lambda-calculus. In Ted Hurley, Mícheál Mac an Airchinnigh, Michel P. Schellekens, and Anthony Karel Seda, editors, First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2000, Cork, Ireland, July 20-21, 2000, volume 40 of Electronic Notes in Theoretical Computer Science, pages 288-301. Elsevier, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80056-8.
  26. Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. Insights From Univalent Foundations: A Case Study Using Double Categories. CoRR, abs/2402.05265, 2024. URL: https://doi.org/10.48550/arXiv.2402.05265.
  27. Egbert Rijke. Introduction to homotopy type theory. arXiv preprint arXiv:2212.11082, 2022. Google Scholar
  28. Ross Street. The formal theory of monads. J. Pure Appl. Algebra, 2(2):149-168, 1972. URL: https://doi.org/10.1016/0022-4049(72)90019-9.
  29. The Coq Development Team. The Coq Proof Assistant, September 2022. URL: https://doi.org/10.5281/zenodo.7313584.
  30. Christopher Francis Townsend. Preframe techniques in constructive locale theory. PhD thesis, Imperial College London (University of London), 1996. Google Scholar
  31. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  32. Dominic Verity. Enriched categories, internal categories and change of base. Repr. Theory Appl. Categ., 20:1-266, 2011. Google Scholar
  33. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. Unimath - a computer-checked library of univalent mathematics. available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.10849216.
  34. Mitchell Wand. Fixed-point constructions in order-enriched categories. Theor. Comput. Sci., 8:13-30, 1979. URL: https://doi.org/10.1016/0304-3975(79)90053-7.
  35. Charles A. Weibel. An introduction to homological algebra, volume 38 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1994. URL: https://doi.org/10.1017/CBO9781139644136.
  36. Niels van der Weide. The formal theory of monads, univalently. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 6:1-6:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.6.
  37. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North. Univalent double categories. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 246-259. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636955.
  38. John Wiegley. category-theory: Category Theory in Coq, 2023. URL: https: //github.com/jwiegley/category-theory.
  39. R. J. Wood. Abstract pro arrows I. Cahiers de topologie et géométrie différentielle, 23(3):279-290, 1982. Google Scholar
  40. Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent monoidal categories. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, volume 269 of LIPIcs, pages 15:1-15:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.TYPES.2022.15.
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