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.