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.