Lemma. Identity type of dirichlet product with FTIT [00EJ]

We present an alternative proof of the characterization of the identity type of the dirichlet product using the fundamental theorem of identity types.

Let and be terms in the dirichlet product of species and . Then there is an equivalence

Proof. See folder.