Commit 2021-01-08 17:23 bd9b03f6

feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624) A re-do of #4929. Re-defines the exponential comparison morphism (now as a natural transformation rather than a morphism with a naturality prop), and defines the Frobenius reciprocity morphism for an adjoint. In the case where the functor has a left adjoint, gives a sufficient condition for it to be cartesian closed, and a sufficient condition for a functor whose left adjoint preserves binary products to be cartesian closed (but doesn't show the necessity of this).

• depends on: #5623