The Conatural Numbers Form an Exponential Commutative Semiring

Conatural numbers are a coinductive type dual to the inductively defined natural numbers. The conatural numbers can represent all natural numbers and an extra element for infinity, this can be useful for representing the amount of steps taken by a possibly non-terminating program. We can define functions on conatural numbers by corecursion, however proof assistants such as Agda require the corecursive definitions to be guarded to make sure that they are productive. This requirement is often too restrictive, as it disallows the corecursive occurrence to appear under previously defined operations. In this paper, we explore some methods to solving this issue using the running examples of multiplication and the commutativity of addition on conatural numbers, then we give comparisons between these methods. As the main result, this is the first proof that conatural numbers form an exponential commutative semiring in cubical type theory without major extensions.