There are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notio

There are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notions of exponentiation, division, subtraction, complement, union, and intersection. There is little formal reason why an algebra of types shouldn’t include even more interesting operations.