Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-20 21:22 94201677

View on Github →

feat(category_theory): unbundled functors and lax monoidal functors (#2193)

feat(category_theory): unbundled functors and lax monoidal functors
doc string

Estimated changes

Modified src/category_theory/functor.lean

Created src/category_theory/functorial.lean

added def category_theory.functor.of

added def category_theory.functorial_comp

added def category_theory.map

added theorem category_theory.map_functorial_obj

Created src/category_theory/monoidal/functorial.lean

added def category_theory.lax_monoidal_functor.of