Zeta Species [00EC]

Given , define

where is the underlying type of . See also Hasse-Weil species in agda-unimath