Cartesian closed categories are distributive

TL;DR

This paper provides an explicit construction of the isomorphism proving that Cartesian closed categories with finite coproducts are distributive, clarifying the involved arrows beyond the usual adjoint functor argument.

Contribution

It offers a detailed, explicit proof of the distributivity of Cartesian closed categories with finite coproducts, enhancing understanding beyond the standard adjoint functor approach.

Findings

Explicit construction of the distributivity isomorphism

Clarification of the involved arrows in the proof

Enhanced understanding of categorical structures

Abstract

A folklore result in category theory is that a (weakly) Cartesian closed category with finite co-products is distributive. Usually, the proof of this small result is carried on using the fact that the exponential functor is right adjoint to the product functor. And, since functors having a right adjoint preserve co-limits, the result follows immediately. But, when we try to explicitly construct the arrows, things become a bit more involved. In rare cases, it is pretty useful to have the exact arrows that make this isomorphism to hold. The purpose of this note is to develop the explicit proof with all the involved arrows constructed in an explicit way.