Commit 2025-06-16 07:03 9ec2bb95

feat(CategoryTheory): pseudofunctors from strict bicategories (#24382) This PR provides an API for pseudofunctors F from a strict bicategory B. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of mapId and mapComp: for example, if f and g are composable morphisms and fg is such that h : fg = f ≫ f, we provide an isomorphism F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square t ≫ r = l ≫ b in B, we construct an isomorphism F.map t ≫ F.map r ≅ F.map l ≫ F.map b.