Nice write up! Ahistorically, if you know some category theory the ideas map directly to what are called sums and products in category theory, and the "category

Nice write up! Ahistorically, if you know some category theory the ideas map directly to what are called sums and products in category theory, and the "category of algebras" is just the special category in which much of the semantics of programming takes place (which is just an abstraction where we have operations just like sum and multiplication, but we can use any set, not just the numbers)—hence types are "algebraic" products and sums.