mathlib documentation


Closed monoidal categories

Define (right) closed objects and (right) closed monoidal categories.


Some of the theorems proved about cartesian closed categories should be generalised and moved to this file.

structure category_theory.closed {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] :
C → Type (max u v)

An object X is (right) closed if (X ⊗ -) is a left adjoint.


A monoidal category C is (right) monoidal closed if every object is (right) closed.

The unit object is always closed. This isn't an instance because most of the time we'll prove closedness for all objects at once, rather than just for this one.