Document Open Access Logo

HoTT Operads

Authors Brandon Hewer , Graham Hutton

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2025.4.pdf
  • Filesize: 0.8 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • operads
  • homotopy type theory
  • proof assistants

Metrics

Abstract

Internalising classes of datatypes has been a longstanding pursuit in type theory. For example, containers capture strictly positive types, while combinatorial species capture finitely labelled structures. To date, however, there has been no similar attempt to internalise classes of operations on datatypes. In this paper we show how the theory of operads, which extend species with a well-behaved notion of composition, provides a natural approach to internalising finitary operations. We present an internalisation of a generalised notion of operad in homotopy type theory, which provides a generic framework for capturing and reasoning about operations with particular algebraic properties. All our results are formalised in Cubical Agda.

Cite As Get BibTex

Brandon Hewer and Graham Hutton. HoTT Operads. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.TYPES.2025.4

Author Details

Brandon Hewer
  • School of Computer Science, University of Nottingham, UK
Graham Hutton
  • School of Computer Science, University of Nottingham, UK

Funding

This work was partially funded by EPSRC grant EP/Y010744/1, Semantics-Directed Compiler Construction: From Formal Semantics to Certified Compilers.

Acknowledgements

The authors thank the reviewers for their constructive feedback and suggestions that have helped to improve this article.

Supplementary Materials

References

  1. Michael Abbott. Categories of Containers. PhD thesis, University of Leicester, 2003. Google Scholar
  2. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing Strictly Positive Types. Theoretical Computer Science, 342(1), 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  3. Michael Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Derivatives of Containers. In International Conference on Typed Lambda Calculi and Applications. Springer, 2003. Google Scholar
  4. HoTT Operads Cubical Agda Library. https://tinyurl.com/y5fbrzdb, 2026. Google Scholar
  5. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. Journal of Functional Programming, 25, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  6. Thorsten Altenkirch, Paul Levy, and Sam Staton. Higher-Order Containers. In Conference on Computability in Europe. Springer, 2010. Google Scholar
  7. John C Baez and James Dolan. Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes. Advances in Mathematics, 135(2):145-206, 1998. Google Scholar
  8. John Michael Boardman and Rainer M Vogt. Homotopy Invariant Algebraic Structures on Topological Spaces, volume 347. Springer, 2006. Google Scholar
  9. Jacques Carette, Chao-Hong Chen, Vikraman Choudhury, and Amr Sabry. From Reversible Programs to Univalent Universes and Back. Electronic Notes in Theoretical Computer Science, 336:5-25, 2018. URL: https://doi.org/10.1016/j.entcs.2018.03.013.
  10. Vikraman Choudhury, Jacek Karwowski, and Amr Sabry. Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages. Proceedings of the ACM on Programming Languages, 6(POPL), 2022. URL: https://doi.org/10.1145/3498667.
  11. J. Daniel Christensen. A Characterization of Univalent Fibrations, 2022. Google Scholar
  12. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  13. Thierry Coquand and Arnaud Spiwack. Constructively Finite? In Contribuciones Científicas en Honor de Mirian Andrés Gómez. Universidad de La Rioja, 2010. Google Scholar
  14. Zachary Flores, Angelo Taranto, Eric Bond, and Yakir Forman. A Formalization of Operads in Coq, 2023. URL: https://doi.org/10.48550/arXiv.2303.08894.
  15. Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide. Finite Sets in Homotopy Type Theory. In International Conference on Certified Programs and Proofs, 2018. Google Scholar
  16. Håkon Robbestad Gylterud. Symmetric Containers. Master’s thesis, University of Oslo, 2011., 2011. Google Scholar
  17. Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, and Thorsten Altenkirch. Small Induction Recursion. In International Conference on Typed Lambda Calculi and Applications, pages 156-172. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_13.
  18. C. Barry Jay and J. Robin B. Cockett. Shapely Types and Shape Polymorphism. In European Symposium on Programming. Springer, 1994. Google Scholar
  19. Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024), pages 6-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.TYPES.2024.6.
  20. André Joyal. Une Théorie Combinatoire des Séries Formelles. Advances in Mathematics, 42(1), 1981. Google Scholar
  21. J Peter May. The Geometry of Iterated Loop Spaces, volume 271. Springer, 2006. Google Scholar
  22. Pierre-Louis Curien, Cédric Ho Thanh, and Samuel Mimram. Syntactic Approaches to Opetopes, 2019. URL: https://arxiv.org/abs/1903.05848.
  23. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proceedings of the ACM on Programming Languages, 3(ICFP), 2019. URL: https://doi.org/10.1145/3341691.
  24. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath: A Computer-Checked Library of Univalent Mathematics. Available at URL: https://github.com/UniMath/UniMath.
  25. Donald Yau. Colored Operads, volume 170. American Mathematical Society, 2016. Google Scholar
  26. Brent Abraham Yorgey. Combinatorial Species and Labelled Structures. PhD thesis, University of Pennsylvania, 2014. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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