FinSet is closed under cartesian products. Proof. See Notebook I.

For finite sets and , we write for finte set that is the cartesian product of and as constructed here.

By abuse of notation we will sometimes just write .

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

Where cartesian product in FinSet.

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

Fix a finite set . There is an equivalence

Where is the induced map from the paths and .

Proof. Denote by the type family .

In the second step, we make use of the rule:

For a path denote by the induced path . then for and we get a term of type

by doing path induction on : When , we get

So it suffices to provide a term of type , which is (up to unit-path) given by reversal of paths.

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

Define by

Note that is a proposition (TODO: write out why) so in particular a set.

Note also that this fits the definition of in the paper quite well.

We prove that

by constructing for each a map

and showing it has contractible fibers.

Proof. A term of type is of the form

where

Note that , so contractible. We denote its center of contraction by . We now define an equivalence

by . Because is contractible, , so is indeed an equivalence.

By univalence gives us a path

Define

Now we show that the fibers of are contracible:

Let . Then the fiber is given by

Define

where is the right unit equivalence and is the identity.

Then

Pick as the center.

We now show that given , with

holds.

Observe, that using (from ), we get that

.

this means we get an element

(that we also call by abuse of notation)

We now use the the characterization of the Identity type of Dirichlet Product, so we only need to give a path

Thus we need

We already have have . Define by applying univalence to . Set . Note that , which is contracible,so

It only reamains to construct . TODO