Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 11:13 b7f8f725

View on Github →

feat(category_theory/bicategory/functor): define oplax functors and their composition (#11277) This PR defines oplax functors between bicategories and their composition.

Estimated changes

Created src/category_theory/bicategory/functor.lean

added def category_theory.oplax_functor.comp

added def category_theory.oplax_functor.id

added def category_theory.oplax_functor.map_functor

added def category_theory.oplax_functor.map₂_associator_aux

added theorem category_theory.oplax_functor.to_prelax_functor_map

added theorem category_theory.oplax_functor.to_prelax_functor_map₂

added theorem category_theory.oplax_functor.to_prelax_functor_obj

added structure category_theory.oplax_functor

added def category_theory.prelax_functor.comp

added def category_theory.prelax_functor.id

added theorem category_theory.prelax_functor.to_prefunctor_map

added theorem category_theory.prelax_functor.to_prefunctor_obj

added structure category_theory.prelax_functor