Cartesian Closed Category - Equational Theory

Equational Theory

In every cartesian closed category (using exponential notation), (XY)Z and (XZ)Y are isomorphic for all objects X, Y and Z. We write this as the "equation"

(xy)z = (xz)y.

One may ask what other such equations are valid in all cartesian closed categories. It turns out that all of them follow logically from the following axioms:

• x×(y×z) = (x×y)×z
• x×y = y×x
• x×1 = x (here 1 denotes the terminal object of C)
• 1x = 1
• x1 = x
• (x×y)z = xz×yz
• (xy)z = x(y×z)

Bicartesian closed categories extend cartesian closed categories with binary coproducts and an initial object, with products distributing over coproducts. Their equational theory is extended with the following axioms:

• x + y = y + x
• (x + y) + z = x + (y + z)
• x(y + z) = xy + xz
• x(y + z) = xyxz
• 0 + x = x
• x×0 = 0
• x0 = 1