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.
a choice of a left adjoint for
tensorLeft X
An object X
is (right) closed if (X ⊗ -)
is a left adjoint.
Instances
- closed : (X : C) → CategoryTheory.Closed X
A monoidal category C
is (right) monoidal closed if every object is (right) closed.
Instances
If X
and Y
are closed then X ⊗ Y
is.
This isn't an instance because it's not usually how we want to construct internal homs,
we'll usually prove all objects are closed uniformly.
Instances For
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.
Instances For
This is the internal hom A ⟶[C] -
.
Instances For
The adjunction between A ⊗ -
and A ⟹ -
.
Instances For
The evaluation natural transformation.
Instances For
The coevaluation natural transformation.
Instances For
A ⟶[C] B
denotes the internal hom from A
to B
Instances For
Currying in a monoidal closed category.
Instances For
Uncurrying in a monoidal closed category.
Instances For
Pre-compose an internal hom with an external hom.
Instances For
The internal hom functor given by the monoidal closed structure.
Instances For
Transport the property of being monoidal closed across a monoidal equivalence of categories
Instances For
Suppose we have a monoidal equivalence F : C ≌ D
, with D
monoidal closed. We can pull the
monoidal closed instance back along the equivalence. For X, Y, Z : C
, this lemma describes the
resulting currying map Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z))
. (X ⟶[C] Z
is defined to be
F⁻¹(F(X) ⟶[D] F(Z))
, so currying in C
is given by essentially conjugating currying in
D
by F.
)
Suppose we have a monoidal equivalence F : C ≌ D
, with D
monoidal closed. We can pull the
monoidal closed instance back along the equivalence. For X, Y, Z : C
, this lemma describes the
resulting uncurrying map Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z)
. (X ⟶[C] Z
is
defined to be F⁻¹(F(X) ⟶[D] F(Z))
, so uncurrying in C
is given by essentially conjugating
uncurrying in D
by F.
)