Types without parameters, $rankType$ and $types$, are defined separately from types over a parameter set, $rankTypeOver$ and $typesOver$. Over the empty set the two agree up to the evident bijection of formulas. The separate version is needed because the formula type of the parameterized version depends on the parameter set, so it would not let one compare types in different structures, such as two induced substructures.

Formulas are those of mathlib's first-order logic, $L.Formula α$, where $α$ indexes the free variables. A parameter from $W$ is a free variable of the right summand of $Fin k ⊕ W$, and it is always assigned the element that it names. This is the same as adjoining a constant for each element of $W$, and it does not change the quantifier rank. The type is literally the set of formulas, as in the paper, and the count is the cardinality of the set of realized types. It is finite whenever $X$ is finite, since it is the image of $X^k$.

The count $typeCountOver$ takes the structure as an explicit argument, because it is applied to structures that are not instances, such as the expansion of a graph by colors.

Mathlib's formulas are built from falsum, equality, relations, implication and universal quantification. The quantifier rank is the nesting depth of the universal quantifier. Every formula of the usual syntax with ¬, ∧, ∨, ∃ and ∀ translates into this syntax without changing its quantifier rank, so the types are the usual ones.