Loogle!

Result

Found 112 declarations mentioning CategoryTheory.Bicategory.Strict.

• CategoryTheory.Bicategory.Strict 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  (B : Type u) [CategoryTheory.Bicategory B] : Prop
• CategoryTheory.StrictBicategory.category 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  (B : Type u) [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] : CategoryTheory.Category.{v, u} B
• CategoryTheory.Bicategory.Strict.comp_id 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f
• CategoryTheory.Bicategory.Strict.id_comp 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f
• CategoryTheory.Bicategory.Strict.assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b) : CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯
• CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b) : CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯
• CategoryTheory.Bicategory.Strict.associator_eqToIso 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} {inst✝ : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯
• CategoryTheory.Bicategory.Strict.mk 📋 Mathlib.CategoryTheory.Bicategory.Strict.Basic
  {B : Type u} [CategoryTheory.Bicategory B] (id_comp : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f := by cat_disch) (comp_id : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f := by cat_disch) (assoc : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) := by cat_disch) (leftUnitor_eqToIso : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯ := by cat_disch) (rightUnitor_eqToIso : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯ := by cat_disch) (associator_eqToIso : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯ := by cat_disch) : CategoryTheory.Bicategory.Strict B
• CategoryTheory.Cat.bicategory.strict 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.Bicategory.Strict CategoryTheory.Cat
• CategoryTheory.Bicategory.instStrictOfIsLocallyDiscrete 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  (B : Type u_1) [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.IsLocallyDiscrete B] : CategoryTheory.Bicategory.Strict B
• CategoryTheory.locallyDiscreteBicategory.strict 📋 Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Bicategory.Strict (CategoryTheory.LocallyDiscrete C)
• CategoryTheory.Functor.toOplaxFunctor' 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete I) B
• CategoryTheory.Functor.toPseudoFunctor' 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B
• CategoryTheory.Functor.toPseudofunctor' 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete I) B
• CategoryTheory.Functor.toOplaxFunctor'_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) : F.toOplaxFunctor'.obj x✝ = F.obj x✝.as
• CategoryTheory.Functor.toPseudofunctor'_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) : F.toPseudofunctor'.obj x✝ = F.obj x✝.as
• CategoryTheory.Functor.toOplaxFunctor'_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toOplaxFunctor'.map x✝ = F.map x✝.as
• CategoryTheory.Functor.toPseudofunctor'_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {X✝ Y✝ : CategoryTheory.LocallyDiscrete I} (x✝ : X✝ ⟶ Y✝) : F.toPseudofunctor'.map x✝ = F.map x✝.as
• CategoryTheory.Functor.toPseudofunctor'_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x✝ : CategoryTheory.LocallyDiscrete I) : F.toPseudofunctor'.mapId x✝ = CategoryTheory.eqToIso ⋯
• CategoryTheory.Functor.toPseudofunctor'_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toPseudofunctor'.mapComp f g = CategoryTheory.eqToIso ⋯
• CategoryTheory.Functor.toOplaxFunctor'_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (a : CategoryTheory.LocallyDiscrete I) : F.toOplaxFunctor'.mapId a = CategoryTheory.eqToHom ⋯
• CategoryTheory.Functor.toOplaxFunctor'_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
  {I : Type u_1} {B : Type u_2} [CategoryTheory.Category.{v_1, u_1} I] [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete I} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toOplaxFunctor'.mapComp f g = CategoryTheory.eqToHom ⋯
• CategoryTheory.CatEnriched.instStrict 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.Bicategory.Strict (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnrichedOrdinary.instStrict 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] : CategoryTheory.Bicategory.Strict (CategoryTheory.CatEnrichedOrdinary C)
• SSet.QCat.strictBicategory 📋 Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
  : CategoryTheory.Bicategory.Strict SSet.QCat
• CategoryTheory.StrictPseudofunctor.mk'' 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) : CategoryTheory.StrictPseudofunctor B C
• CategoryTheory.StrictPseudofunctor.toFunctor 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (F : CategoryTheory.StrictPseudofunctor B C) : CategoryTheory.Functor B C
• CategoryTheory.StrictPseudofunctor.toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (F : CategoryTheory.StrictPseudofunctor B C) (a✝ : B) : F.toFunctor.obj a✝ = F.obj a✝
• CategoryTheory.StrictPseudofunctor.mk''_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) (a✝ : B) : (CategoryTheory.StrictPseudofunctor.mk'' S).obj a✝ = S.obj a✝
• CategoryTheory.StrictPseudofunctor.toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (F : CategoryTheory.StrictPseudofunctor B C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : F.toFunctor.map a✝ = F.map a✝
• CategoryTheory.StrictPseudofunctor.mk''_map 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) : (CategoryTheory.StrictPseudofunctor.mk'' S).map a✝ = S.map a✝
• CategoryTheory.StrictPseudofunctor.mk''_map₂ 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : (CategoryTheory.StrictPseudofunctor.mk'' S).map₂ a✝¹ = S.map₂ a✝¹
• CategoryTheory.StrictPseudofunctor.mk''_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) (x : B) : (CategoryTheory.StrictPseudofunctor.mk'' S).mapId x = CategoryTheory.eqToIso ⋯
• CategoryTheory.StrictPseudofunctor.mk''_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
  {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory.Strict C] (S : CategoryTheory.StrictPseudofunctorPreCore B C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (CategoryTheory.StrictPseudofunctor.mk'' S).mapComp f g = CategoryTheory.eqToIso ⋯
• CategoryTheory.Bicategory.InducedBicategory.instStrict 📋 Mathlib.CategoryTheory.Bicategory.InducedBicategory
  {B : Type u_1} {C : Type u_2} [CategoryTheory.Bicategory C] {F : B → C} [CategoryTheory.Bicategory.Strict C] : CategoryTheory.Bicategory.Strict (CategoryTheory.Bicategory.InducedBicategory C F)
• CategoryTheory.Pseudofunctor.isoMapOfCommSq 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ Y₁ Y₂ : B} {t : X₁ ⟶ Y₁} {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CategoryTheory.CommSq t l r b) : CategoryTheory.CategoryStruct.comp (F.map t) (F.map r) ≅ CategoryTheory.CategoryStruct.comp (F.map l) (F.map b)
• CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ Y₁ Y₂ : B} {t : X₁ ⟶ Y₁} {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CategoryTheory.CommSq t l r b) (φ : X₁ ⟶ Y₂) (hφ : CategoryTheory.CategoryStruct.comp t r = φ) : F.isoMapOfCommSq sq = (F.mapComp' t r φ ⋯).symm ≪≫ F.mapComp' l b φ ⋯
• CategoryTheory.Pseudofunctor.mapComp'_comp_id 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯ = (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫ CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b₁).symm
• CategoryTheory.Pseudofunctor.mapComp'_id_comp 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯ = (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫ CategoryTheory.Bicategory.whiskerRightIso (F.mapId b₀).symm (F.map f)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom) (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).inv (F.map f))
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) : (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).hom (F.map f)) (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) {Z : F.obj b₀ ⟶ F.obj b₁} (h : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.CategoryStruct.id b₁)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).inv) h)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) {Z : F.obj b₀ ⟶ F.obj b₁} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom h)
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) {Z : F.obj b₀ ⟶ F.obj b₁} (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id b₀)) (F.map f) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).inv (F.map f)) h)
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁) {Z : F.obj b₀ ⟶ F.obj b₁} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).hom (F.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom h)
• CategoryTheory.Pseudofunctor.isoMapOfCommSq_horiz_id 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ : B} (f : X₁ ⟶ X₂) : F.isoMapOfCommSq ⋯ = CategoryTheory.Bicategory.whiskerRightIso (F.mapId X₁) (F.map f) ≪≫ CategoryTheory.Bicategory.leftUnitor (F.map f) ≪≫ (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫ (CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂)).symm
• CategoryTheory.Pseudofunctor.isoMapOfCommSq_vert_id 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {X₁ X₂ : B} (f : X₁ ⟶ X₂) : F.isoMapOfCommSq ⋯ = CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId X₂) ≪≫ CategoryTheory.Bicategory.rightUnitor (F.map f) ≪≫ (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫ (CategoryTheory.Bicategory.whiskerRightIso (F.mapId X₁) (F.map f)).symm
• CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp' 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (F.mapComp' f₀₁ f₁₃ f hf) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯))
• CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp' 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (F.mapComp' f₀₁ f₁₃ f ⋯))
• CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp' 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
• CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) : (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F.mapId b₁).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) : (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.mapId b₁).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h))
• CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (CategoryTheory.CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) h) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
• CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) h))
• CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃)) h) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) : (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F.map f).toFunctor.map ((F.mapId b₀).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) : (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId b₀).hom.toNatTrans.app X)) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : (F.mapComp' f₀₁ f₁₃ f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯).inv))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : (F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (F.mapComp' f₀₁ f₁₃ f ⋯).inv))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (F.mapComp' f₀₁ f₁₃ f hf).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯).inv)
• CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (F.mapComp' f₀₁ f₁₃ f hf).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯).inv)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : (F.mapComp' f₀₁ f₁₃ f ⋯).hom = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)))
• CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_comp_mapComp'_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (F.mapComp' f₀₁ f₁₃ f ⋯).inv)
• CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (F.mapComp' f₀₂ f₂₃ f ⋯).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (F.mapComp' f₀₁ f₁₃ f ⋯).inv)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : (F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))))
• CategoryTheory.Pseudofunctor.mapComp'_inv_comp_mapComp'_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (F.mapComp' f₀₂ f₂₃ f ⋯).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)))
• CategoryTheory.Pseudofunctor.mapComp'_hom_comp_mapComp'_hom_whiskerRight 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv (F.mapComp' f₀₁ f₁₃ f ⋯).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv))
• CategoryTheory.Pseudofunctor.mapComp'_hom_comp_whiskerLeft_mapComp'_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)} (h : (F.map (CategoryTheory.CategoryStruct.id b₁)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.mapId b₁).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h)
• CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.mapId b₁).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h)))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h)))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h)))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h)))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₂) (F.map f₂₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) h))
• CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).inv h))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₂)) (F.map f₂₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) h) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv h))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (F.map f₁₃) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv) h))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u₁} {C : Type u₂} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : CategoryTheory.CategoryStruct.comp (F.map f₀₁) (CategoryTheory.CategoryStruct.comp (F.map f₁₂) (F.map f₂₃)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom) h) = CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom h))
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)} (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id b₀)).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId b₀).inv.toNatTrans.app X)) h)
• CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId b₀).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) : (F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) : (F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) : (F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) : (F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) ((F.mapComp' f₀₁ f₁₃ f hf).inv.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) ((F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₁₃).toFunctor.obj ((F.map f₀₁).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h))
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₀₂).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) h))
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f hf).inv.toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₀₂).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) h)
• CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₁₂).toFunctor.obj ((F.map f₀₁).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) h) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₁₃).toFunctor.obj ((F.map f₀₁).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h)
• CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₁₂).toFunctor.obj ((F.map f₀₁).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ ⋯).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h) = CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) h)
• CategoryTheory.BasedCategory.instStrict 📋 Mathlib.CategoryTheory.FiberedCategory.BasedCategory
  {𝒮 : Type u₁} [CategoryTheory.Category.{v₁, u₁} 𝒮] : CategoryTheory.Bicategory.Strict (CategoryTheory.BasedCategory 𝒮)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 401c76f serving mathlib revision a3d2529