Constructive Final Semantics of Finite Bags

Authors Philipp Joram , Niccolò Veltri

Thumbnail PDF


  • Filesize: 0.82 MB
  • 19 pages

Document Identifiers

Author Details

Philipp Joram
  • Department of Software Science, Tallinn University of Technology, Estonia
Niccolò Veltri
  • Department of Software Science, Tallinn University of Technology, Estonia

Cite AsGet BibTex

Philipp Joram and Niccolò Veltri. Constructive Final Semantics of Finite Bags. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Finitely-branching and unlabelled dynamical systems are typically modelled as coalgebras for the finite powerset functor. If states are reachable in multiple ways, coalgebras for the finite bag functor provide a more faithful representation. The final coalgebra of this functor is employed as a denotational domain for the evaluation of such systems. Elements of the final coalgebra are non-wellfounded trees with finite unordered branching, representing the evolution of systems starting from a given initial state. This paper is dedicated to the construction of the final coalgebra of the finite bag functor in homotopy type theory (HoTT). We first compare various equivalent definitions of finite bags employing higher inductive types, both as sets and as groupoids (in the sense of HoTT). We then analyze a few well-known, classical set-theoretic constructions of final coalgebras in our constructive setting. We show that, in the case of set-based definitions of finite bags, some constructions are intrinsically classical, in the sense that they are equivalent to some weak form of excluded middle. Nevertheless, a type satisfying the universal property of the final coalgebra can be constructed in HoTT employing the groupoid-based definition of finite bags. We conclude by discussing generalizations of our constructions to the wider class of analytic functors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
  • finite bags
  • final coalgebra
  • homotopy type theory
  • Cubical Agda


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


  1. Michael Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Constructing polymorphic programs with quotient types. In Dexter Kozen and Carron Shankland, editors, Proc. of 7th Int. Conf. on Mathematics of Program Construction, MPC'04, volume 3125 of LNCS, pages 2-15. Springer, 2004. URL:
  2. Jirí Adámek and Václav Koubek. On the greatest fixed point of a set functor. Theoretical Computer Science, 150(1):57-75, 1995. URL:
  3. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in Homotopy Type Theory. In Thorsten Altenkirch, editor, Proc. of 13th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'15, volume 38 of LIPIcs, pages 17-30. Schloss Dagstuhl, 2015. URL:
  4. Michael Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer Science, 114(2):299-315, 1993. URL:
  5. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13(2):261-293, 2003. URL:
  6. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. Cambridge University Press, 1987. URL:
  7. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of higher truncations. In Stephan Kreutzer, editor, Proc. of 24th EACSL Ann. Conf. on Computer Science Logic, CSL'15, volume 41 of Leibniz International Proceedings in Informatics, pages 359-373. Schloss Dagstuhl, 2015. URL:
  8. Vikraman Choudhury and Marcelo Fiore. Free commutative monoids in homotopy type theory. In Proc. of 38th Conf. on Mathematical Foundations of Programming Semantics (MFPS XXXVIII), volume 1. Centre pour la Communication Scientifique Directe (CCSD), 2023. URL:
  9. Vikraman Choudhury, Jacek Karwowski, and Amr Sabry. Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages. Proc. of the ACM on Programming Languages, 6(POPL):1-32, 2022. URL:
  10. Eric Finster, Samuel Mimram, Maxime Lucas, and Thomas Seiller. A cartesian bicategory of polynomial functors in homotopy type theory. In Ana Sokolova, editor, Proc. of 37th Conf. on Mathematical Foundations of Programming Semantics, MFPS'21, volume 351 of EPTCS, pages 67-83, 2021. URL:
  11. Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide. Finite sets in homotopy type theory. In June Andronick and Amy P. Felty, editors, Proc. of 7th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP'18, pages 201-214. ACM, 2018. URL:
  12. Ryu Hasegawa. Two applications of analytic functors. Theoretical Computer Science, 272(1-2):113-175, 2002. URL:
  13. Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive predicates and final sequences in a fibration. In Dexter Kozen and Michael W. Mislove, editors, Proc. of the 29th Conf. on the Mathematical Foundations of Programming Semantics, MFPS'13, volume 298 of ENTCS, pages 197-214. Elsevier, 2013. URL:
  14. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL:
  15. André Joyal. Foncteurs analytiques et espèces de structures. In Combinatoire énumérative, pages 126-159. Springer Berlin Heidelberg, 1986. URL:
  16. Joachim Kock. Data Types with Symmetries and Polynomial Functors over Groupoids. In Ulrich Berger and Michael Mislove, editors, Proc. of 28th Conf. on Mathematical Foundations of Programming Semantics, MFPS'12, volume 286 of ENTCS, pages 351-365. Elsevier, 2012. URL:
  17. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science, 13(1), 2017. URL:
  18. Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. In Christel Baier and Dana Fisman, editors, Proc. of 37th Ann. ACM/IEEE Symp. on Logic in Computer Science, LICS'22, pages 42:1-42:13. ACM, 2022. URL:
  19. Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Proc. of 14th Int. Conf on Foundations of Software Science and Computational Structures, FoSSaCS'11, volume 6604 of LNCS, pages 27-41. Springer, 2011. URL:
  20. Nuo Li. Quotient types in type theory. PhD thesis, University of Nottingham, UK, 2015. URL:
  21. Mark Mandelkern. Constructively complete finite sets. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 34(2):97-103, 1988. URL:
  22. Stefano Piceghello. Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory. PhD thesis, University of Bergen, Norway, 2021. URL:
  23. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. URL:
  24. Kristina Sojakova. Higher Inductive Types as Homotopy-Initial Algebras. PhD thesis, Carnegie Mellon University, USA, 2016. URL:
  25. The agda/cubical development team. The agda/cubical library, 2018. URL:
  26. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics., Institute for Advanced Study, 2013.
  27. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. of 12th Ann. IEEE Symp. on Logic in Computer Science, LICS'97, pages 280-291. IEEE Computer Society, 1997. URL:
  28. Niccolò Veltri and Niels van der Weide. Constructing higher inductive types as groupoid quotients. Logical Methods in Computer Science, 17(2), 2021. URL:
  29. Niccolò Veltri. Type-theoretic constructions of the final coalgebra of the finite powerset functor. In Naoki Kobayashi, editor, Proc. of 6th Int. Conf. on Formal Structures for Computation and Deduction, FSCD'21, volume 195 of LIPIcs, pages 22:1-22:18. Schloss Dagstuhl, 2021. URL:
  30. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Proc. of the ACM on Programming Languages, 3(ICFP):1-29, 2019. URL:
  31. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. URL:
  32. James Worrell. On the final sequence of a finitary set functor. Theoretical Computer Science, 338(1-3):184-199, 2005. URL:
  33. Brent Yorgey. Combinatorial Species and Labelled Structures. PhD thesis, University of Pennsylvania, 2014. URL:
  34. Brent A. Yorgey. Species and functors and types, oh my! In Jeremy Gibbons, editor, Proc. of 3rd ACM Symp. on Haskell, Haskell'10, pages 147-158. ACM, 2010. URL: