Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-06 07:44 371b48a0

View on Github →

feal(category_theory/bicategory/functor): define pseudofunctors (#11992) This PR defines pseudofunctors between bicategories. We provide two constructors (mk_of_oplax and mk_of_oplax') that construct pseudofunctors from oplax functors whose map_id and map_comp are isomorphisms. The constructor mk_of_oplax uses iso to describe isomorphisms, while mk_of_oplax' uses is_iso.

Estimated changes

Modified src/category_theory/bicategory/functor.lean

modified def category_theory.oplax_functor.comp

modified def category_theory.oplax_functor.id

added structure category_theory.oplax_functor.pseudo_core

added theorem category_theory.oplax_functor.to_prelax_eq_coe

modified theorem category_theory.oplax_functor.to_prelax_functor_map

modified theorem category_theory.oplax_functor.to_prelax_functor_map₂

modified theorem category_theory.oplax_functor.to_prelax_functor_obj

modified structure category_theory.oplax_functor

modified def category_theory.prelax_functor.comp

modified def category_theory.prelax_functor.id

added theorem category_theory.prelax_functor.to_prefunctor_eq_coe

modified theorem category_theory.prelax_functor.to_prefunctor_map

modified theorem category_theory.prelax_functor.to_prefunctor_obj

modified structure category_theory.prelax_functor

added def category_theory.pseudofunctor.comp

added def category_theory.pseudofunctor.id

added def category_theory.pseudofunctor.map_functor

added def category_theory.pseudofunctor.map₂_associator_aux

added def category_theory.pseudofunctor.mk_of_oplax'

added def category_theory.pseudofunctor.mk_of_oplax

added def category_theory.pseudofunctor.to_oplax

added theorem category_theory.pseudofunctor.to_oplax_eq_coe

added theorem category_theory.pseudofunctor.to_oplax_map

added theorem category_theory.pseudofunctor.to_oplax_map_comp

added theorem category_theory.pseudofunctor.to_oplax_map_id

added theorem category_theory.pseudofunctor.to_oplax_map₂

added theorem category_theory.pseudofunctor.to_oplax_obj

added theorem category_theory.pseudofunctor.to_prelax_functor_eq_coe

added theorem category_theory.pseudofunctor.to_prelax_functor_map

added theorem category_theory.pseudofunctor.to_prelax_functor_map₂

added theorem category_theory.pseudofunctor.to_prelax_functor_obj

added structure category_theory.pseudofunctor