 In type theory, the general idea of a type system in computer science is formalized into a specific algebra of types.For example, when writing formula_44, the intent is that formula_3 and formula_4 are types, while the arrow formula_132 is a type constructor, specifically, the function type or arrow type.Similarly, the Cartesian product formula_45 of types is constructed by the product type constructor formula_134.