This note attempts to state a HoTTification of the key results from the paper Dirichlet Species and Arithmetic Zeta Functions. Some things I say here may simply be wrong because I have not proved most of what I am claiming here. This serves more as a roadmap than as a collection of results.

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

See the paper

A categorification of this is the -Dirichlet series defined for with by

See Dirichlet series of species of types in agda-unimath

It is not quite clear to me how this unifies what should happen to s and -s -> TODO.

Given a function we get a species as follows. A structure on a finite set is a way of making it into a simisimple commutative ring and picking an element of .

This is called the Hasse-Weil species

For a HoTTification see Hasse-Weil species in agda-unimath

• Artin-Wedderburn Theorem

Finite semisimple commutative ring is the same as a finite product of finite fields. –> Pobably "just" isomorphism of types

The Dirichlet series of the hasse-weil species is equal to the usual hasse-weil zeta function. –> How do we say this in HoTT, in particular, how do we category the hasse-weil zeta function for a given X nicely?

generalization to stuff types –> (in n-lab entry but not paper) –> some of this is present in agda-unimath

• this feels very similar to what we are doing to species in HoTT already
• groupoid cardinality instead of cardinality
• dirichlet series
• multiplicative species generalize to multiplicative stuff types

–> allegedly these too have dirichlet series admitting euler factorizations.