mathlib documentation

category_theory.monoidal.types.coyoneda

(πŸ™_ C ⟢ -) is a lax monoidal functor to Type #