Coinductive Control of Inductive Data Types

Authors Paige Randall North, Maximilien Péroux

Thumbnail PDF


  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Paige Randall North
  • Department of Mathematics and Department of Information and Computing Sciences, Utrecht University, The Netherlands
Maximilien Péroux
  • Department of Mathematics, University of Pennsylvania, Philadelphia, PA, USA

Cite AsGet BibTex

Paige Randall North and Maximilien Péroux. Coinductive Control of Inductive Data Types. In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched in the corresponding category of coalgebras of the same endofunctor. The enrichment captures all possible partial algebra homomorphisms, defined by measuring coalgebras. Thus this enriched category carries more information than the usual category of algebras which captures only total algebra homomorphisms. We specify new algebras besides the initial one using a generalization of the notion of initial algebra.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Algebraic semantics
  • Theory of computation → Type structures
  • Inductive types
  • enriched category theory
  • algebraic data types
  • algebra
  • coalgebra


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


  1. Jiří Adámek and Hans-E. Porst. On varieties and covarieties in a category. Mathematical Structures in Computer Science, 13(2):201-232, 2003. URL:
  2. Jiří Adámek and Jiří Rosický. Locally presentable and accessible categories, volume 189 of London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 1994. URL:
  3. Martin Hyland, Ignacio López Franco, and Christina Vasilakopoulou. Hopf measuring comonoids and enrichment. Proc. Lond. Math. Soc. (3), 115(5):1118-1148, 2017. URL:
  4. Jacob Lurie. Higher topos theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2009. URL:
  5. Per Martin-Löf. Intuitionistic type theory. Naples: Bibliopolis, 1984. Google Scholar
  6. Dylan McDermott, Exequiel Rivas, and Tarmo Uustalu. Sweedler theory of monads. In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures, pages 428-448, Cham, 2022. Springer International Publishing. URL:
  7. Paige Randall North and Maximilien Péroux. Coinductive control of inductive data types, 2023. URL:
  8. Maximilien Péroux. The coalgebraic enrichment of algebras in higher categories. Journal of Pure and Applied Algebra, 226(3):106849, 2022. URL:
  9. Jan Rutten. The Method of Coalgebra: exercises in coinduction. C, 2019. URL:
  10. Moss E. Sweedler. Hopf algebras. Mathematics Lecture Note Series. W. A. Benjamin, Inc., New York, 1969. Google Scholar
  11. Christina Vasilakopoulou. Enriched duality in double categories: 𝒱-categories and 𝒱-cocategories. J. Pure Appl. Algebra, 223(7):2889-2947, 2019. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail