Commit 2024-06-30 08:05 7d9b08cd

View on Github →

feat(Bicategory/Functor): add OplaxFunctor.map₂Iso and Pseudofunctor.map₂Iso (#13900) This PR adds OplaxFunctor.map₂Iso and Pseudofunctor.map₂Iso, analogous to Functor.mapIso, and develops the corresponding API.

Estimated changes

Modified Mathlib/CategoryTheory/Bicategory/Functor/Oplax.lean

added theorem CategoryTheory.OplaxFunctor.map₂_hom_inv

added theorem CategoryTheory.OplaxFunctor.map₂_inv

added theorem CategoryTheory.OplaxFunctor.map₂_inv_hom

Modified Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

added theorem CategoryTheory.Pseudofunctor.map₂_hom_inv

added theorem CategoryTheory.Pseudofunctor.map₂_inv

added theorem CategoryTheory.Pseudofunctor.map₂_inv_hom