Lemma. Identity type of Dirichlet Product [00E4]

Let and be terms in the dirichlet product of species and .

Let be indexed by the type of cartesian decompositions, then

Proof.

Given , define . We then have that

We make use of the following charcterization of the idenity type of cartesian decompositions constructed here, and denote it by .

With that the equivalence becomes

Here we are using that, given some equivalence of types , we get an equivalence .

Now since is constant in we have by this lemma, that

We conclude that