Documentation

Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

(𝟙_ C ⟶ -) is a lax monoidal functor to Type #

source
noncomputable def CategoryTheory.coyonedaTensorUnit (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] :
CategoryTheory.LaxMonoidalFunctor C (Type v)

(𝟙_ C ⟶ -) is a lax monoidal functor to Type.

Equations
  • One or more equations did not get rendered due to their size.
Instances For