« Dirichlet Product of Species

Definition. cartesian decomposition [00DQ]

Given a finite set , we define the type of cartesian decompositions by

Where cartesian product in FinSet.

Backlinks

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