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.