Proposition. [00BD]

Let and be species of types. The cauchy exponential fullfills the following identity.

Proof. We give an equivalence by contructing maps and that are mutual inverses.

Forward map . Given an element of the LHS i.e a term with

we need write as a binary coproduct such that we can put an exp-structure on each summand.

We start by splitting into subtypes and as follows. TODO: are these actually subtypes?

Now we choose our summands as

Since , we can upgrade to an equivalence equivalence .

Now we want to place an - and -structure on and repectively. For this we need to construct the remaining terms.

Now

This completes our construction of . Notice that

Reverse map . We are given an element with

, define

then

giving . Define

And .

TODO: Make sure and really compose to the identity both ways.