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

    where is the equivalence characterizing the identity type of cart-dec.

    In the second step we are using that, given some equivalence of types , we get an equivalence

    In the third step we are using the follwing. Given any , we have

    TODO is this true? (third step):

    • spell this out using path induction.
    • here is again the equivalence characterizing the identity type of cart-dec.
    • A(T,U,e) ignores e