The algebra of types is a semiring, which is a generalization of a ring that drops the requirement of an additive inverse, just as a ring is a generalization of

The algebra of types is a semiring, which is a generalization of a ring that drops the requirement of an additive inverse, just as a ring is a generalization of a field that doesn’t require a multiplicative inverse. Semirings are pretty common in math – hell, natural numbers form (only) a semiring, having neither type of inverse! Can’t get more fundamental than that. And of course the connection between naturals (counting numbers) and types is evident from the fact that we started this whole exercise by counting inhabitants and defining equivalent based on that!