DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2025.4

HoTT Operads

Authors: Brandon Hewer and Graham Hutton

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{hewer_et_al:LIPIcs.TYPES.2025.4,
  author =	{Hewer, Brandon and Hutton, Graham},
  title =	{{HoTT Operads}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.4},
  URN =		{urn:nbn:de:0030-drops-270228},
  doi =		{10.4230/LIPIcs.TYPES.2025.4},
  annote =	{Keywords: operads, homotopy type theory, proof assistants}
}

Search Results

Documents authored by Hutton, Graham

HoTT Operads

Abstract

Cite as

Thanks for your feedback!

Could not send message