Multi-Sorted Finitary Signature

A multi-sorted finitary signature consists of a type of sorts $S:\mathsf{U}{}$, along with a family $F:S^{*}\to S\to\mathsf{U}{}$.

More abstractly, a multi-sorted finitary signature is an object of the Pullback of the Family Fibration $\mathrm{Fam}{.}({\mathrm{Sets}{.}})$ along the functor $X\mapsto X^{*}\times X$.

References

• Categorical Logic and Type Theory, Section 1.6