Contents

{-# OPTIONS --guardedness --sized-types #-}
module Introduction.index where

This document is a support Agda formalisation a paper currently under review. We develop a fragment of the theory of formal series in noncommuting variables and their algebraic properties. Our approach is coinductive, using Agda’s sized types and guardedness features.

Organisation

The rest of the document is structured as follows. In the Preliminaries part, we introduce some basic notions extending Agda’s standard library. Then in the General part, we develop some aspects of the theory of formal series which are valid for every product rule. Finally, in the Special part, we develop the aspects of the theory of formal series which holds only for special product rules.

import Preliminaries.index
import General.index
import Special.index

Acknowledgements

The following two projects have been inspiring for this document.

  • [Kirst and Zeng(2025)] shows an example of a mathematical paper containing hyperlinks to a supporting Coq formalisation.
  • [Wadler, Kokke, and Siek(2020)] shows that beautiful books can be written in Agda. A lot of the layout in this document is inspired from this project.

The following are some basic Agda resources:

References

[Bove and Dybjer(2008)] A Bove and P Dybjer. Dependent types at work. In A Bove et al., editors., Language engineering and rigorous software development, pages 57–99. Springer-Verlag, Berlin, Heidelberg, 2008.

[Dybjer(2018)] P Dybjer. An introduction to programming and proving in agda.

[Kirst and Zeng(2025)] D Kirst and H Zeng. The blurred drinker paradox: Constructive reverse mathematics of the downward löwenheim-skolem theorem. 2025 40th annual ACM/IEEE symposium on logic in computer science (LICS) (June.-2025), 926–940.

[McBride(2013)] C McBride. Dependently typed metaprogramming (in agda).

[Norell(2009)] U Norell. Dependently typed programming in agda. Proceedings of the 6th international conference on advanced functional programming (Berlin, Heidelberg, 2009), 230–266.

[Stump(2016)] A Stump. Verified functional programming in agda. ACM Books, 2016.

[Wadler et al.(2020)] P Wadler et al. Programming language foundations in Agda. July 2020.