Documentation

Mathlib.CategoryTheory.Adjunction.Evaluation

Adjunctions involving evaluation #

We show that evaluation of functors have adjoints, given the existence of (co)products.

The adjunction showing that evaluation is a right adjoint.

Instances For

    The adjunction showing that evaluation is a left adjoint.

    Instances For