Finite groupoid cardinality and homotopy-fiber integration

The groupoid cardinality and integral in the Definition are finite sums by [A1]. Fix $d\in \mathcal{D}$ and one representative $c$ from each source isomorphism class. The set of isomorphisms $p(c)\cong d$ is empty or a torsor for the finite group ${\mathrm{Aut}}_{\mathcal{D}}(d)$. Every object of the homotopy fiber is isomorphic to one with such a chosen source representative, so the fiber has finitely many isomorphism classes. The automorphisms of $(c,\alpha )$ are the $u\in {\mathrm{Aut}}_{\mathcal{C}}(c)$ satisfying $\alpha \circ p(u)=\alpha$, a subgroup of a finite group by [A1]. Thus every homotopy fiber is finite and each pushforward sum is finite.

If $\eta :d\to d^{\mathrm{\prime }}$ is an isomorphism in $\mathcal{D}$, the rule $(c,\alpha )\mapsto (c,\eta \circ \alpha )$ is an equivalence ${\mathcal{C}}_d\to {\mathcal{C}}_{d^{\mathrm{\prime }}}$ with inverse given by ${\eta }^{-1}$. It preserves isomorphism classes, automorphism groups, and the values of $f([c])$, so the fiber integral is independent of the representative of $[d]$.

If $c\to c^{\mathrm{\prime }}$ is an isomorphism in $\mathcal{C}$, then $p(c)\to p(c^{\mathrm{\prime }})$ is an isomorphism in $\mathcal{D}$, so $p^{\ast }g$ is invariant; step 1.2 proves the same for $p_{!}f$. Consequently $b_{!}{a}^{\ast }$ is a well-defined linear map, since its sums are finite and both operations preserve linear combinations.