« Overview

Definition. Species on FinSet [00DT]

A species is a function , where is the groupoid of finite sets and bijections.

Backlinks

Definition. Dirichlet Product Species [00DP]

Given species define the dirichlet product by

where is the type of cartesian decompositions of .

Lemma. 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

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

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.