2026-07-30T14:29:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27022 2026-07-30T09:16:25Z ddc:004 open_access

HoTT Operads Hewer, Brandon Hutton, Graham operads homotopy type theory proof assistants 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Brandon Hewer and Graham Hutton 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.4 urn:nbn:de:0030-drops-270228 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.4 eng https://creativecommons.org/licenses/by/4.0/legalcode