Dirichlet Series [00EB]

Given a species we obtain a dirichlet series , classically given by

See the paper. A categorification of this is the -Dirichlet series in agda-unimath defined for with by

Evidentily this is a good definition to recover a lot of algebraic properties of the dirichlet product, as has been done in agda unimath.

For , consider , where is the cardinality of , and the delooping of the cyclic group in elements. Then this could be a nice categorification of the dirichlet series, since the groupoid cardinality of is

Note though that is not multiplicative in the sense of the -Dirichlet series. E.g.

But we still get multiplicativity of cardinalities (hopefully), since

Define the categorified version of the dirichlet series to be

the we can decategorigy by taking the groupoid cardinality (in the case where F is wellbehaved) TODO : elaborate on constraints

-> Still need to work out how to take the groupoidcardinality in HoTT and in which cases this is well-defined.