📝Category Theory: Product

tags

§ Category Theory

Universal construction:

$P, \pi_1, \pi_2$ is the (categorical) product of $A$ and $B$ if $\pi_1 : P \to A$ and $\pi_2 : P \to B$ and $\forall(X, f_1 : X \to A, f_2 : X \to B)\; \exists! f : X \to P \ni \pi_1 \circ f = f_1, \pi_2 \circ f = f_2$

Also:

• $P$ is usually called $A\times B$ or in types: $(A,B)$

• $\pi_1$ and $\pi_2$ are called projections.

Terminal object is a unit value of categorical product ($a\times() \cong a$) (forming a Monoid and Cartesian monoidal category).

Backlinks

• 📝 Category Theory: Coproduct
• 📝 Cartesian monoidal category
• 📝 § Category Theory