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 structure category_theory.oplax_functor
modified structure category_theory.prelax_functor