Combinatorial Class

A combinatorial class is a Countable Type $A$ equipped with a function $|-|:A\to\mathbb{N}$ such that the fibre of $|-|$ over every $n:\mathbb{N}$ is Finite.

In terms of dependent type theory, a combinatorial class is a $\mathbb{N}$-indexed family of finite sets $A:\mathbb{N}\to\mathsf{FinSet}$.

Counting sequences

The counting sequence of a combinatorial class is a sequence $\mathbb{N}\to\mathbb{N}$ given by $\lambda n.\;|A(n)|$.

Examples

• The product of two combinatorial classes $A\times B$ is given by
• The unit class is the combinatorial class given by

  $\par\mathcal{E}=\begin{cases}\top&n=0\\ \bot&n\neq 0\end{cases}\par$

Properties

• A combinatorial class is a Polynomial Functor indexed by $\mathbb{N}$ where each fibre is Finite.

References

• Flajolet, Philippe, and Robert Sedgewick. Analytic Combinatorics. 4th pr. Cambridge: Cambridge Univ. Press, 2013.