# mathlibdocumentation

category_theory.closed.monoidal

# Closed monoidal categories #

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

## TODO #

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

@[class]
structure category_theory.closed {C : Type u} (X : C) :
Type (max u v)

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

Instances
@[class]
structure category_theory.monoidal_closed (C : Type u)  :
Type (max u v)
• closed : Π (X : C),

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

Instances
def category_theory.unit_closed {C : Type u}  :

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.

Equations