mathlib3 documentation

category_theory.monoidal.types.coyoneda

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.