NOTE: This site has just upgraded to Forester 5.x and is still having some style and functionality issues, we will fix them ASAP.

lemma. properties of cartesian closed categories [kostecki2011introduction, 5.15] [tt-004N]
✍️source

     For any cartesian closed category \({\cal C}\), and any objects \(X, Y, Z\) of \({\cal C}\), we have
    1. \(\mathrm {0} \times X \cong \mathrm {0}\) if \(\mathrm {0}\) exists in \({\cal C}\)
    2. \(1 \times X \cong X\)
    3. \(X^{\mathrm {0}} \cong \mathrm {1}\) if \(\mathrm {0}\) exists in \({\cal C}\)
    4. \(X^1 \cong X\)
    5. \(\mathrm {1}^X \cong 1\)
    6. \(X \times Y \cong Y \times X\)
    7. \((X \times Y) \times Z \cong X \times (Y \times Z)\)
    8. \(Y^X \times Z^X \cong (Y \times Z)^X\)
    9. \(Z^{X \times Y} \cong \left (Z^X\right )^Y\)
    10. \(X+Y \cong Y+X\)
    11. \((X+Y)+Z \cong X+(Y+Z)\)
    12. \(Z^X \times Z^Y \cong Z^{X+Y}\) if \({\cal C}\) has binary coproducts
    13. \((X \times Y)+(X \times Z) \cong X \times (Y+Z)\) if \({\cal C}\) has binary coproducts