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.

hello world

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.

see folder.

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

Let and be terms in the dirichlet product of species and .

Let be indexed by the type of cartesian decompositions, then

Proof.

Given , define . We then have that

We make use of the following charcterization of the idenity type of cartesian decompositions constructed here, and denote it by .

With that the equivalence becomes

Here we are using that, given some equivalence of types , we get an equivalence .

Now since is constant in we have by this lemma, that

We conclude that

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.

Define by

Note that is a proposition (TODO: explain) 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: copy from Notebook II)

Given species on FinSet and we have that

Proof. TODO: just rearranging things

Proof. TODO

TODO: Look into the definition of symmetric monoidal, figure out what else there is to show here (i.e coherence stuff). Conclude.

i.e