Pseudofunctors

A pseudofunctor is an oplax (or lax) functor whose mapId and mapComp are isomorphisms. We provide several constructors for pseudofunctors:

• Pseudofunctor.mk : the default constructor, which requires map₂_whiskerLeft and map₂_whiskerRight instead of naturality of mapComp.

• Pseudofunctor.mkOfOplax : construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms. This constructor uses Iso to describe isomorphisms.

• pseudofunctor.mkOfOplax' : similar to mkOfOplax, but uses IsIso to describe isomorphisms.

• Pseudofunctor.mkOfLax : construct a pseudofunctor from a lax functor whose mapId and mapComp are isomorphisms. This constructor uses Iso to describe isomorphisms.

• pseudofunctor.mkOfLax' : similar to mkOfLax, but uses IsIso to describe isomorphisms.

Main definitions

• CategoryTheory.Pseudofunctor B C : a pseudofunctor between bicategories B and C
• CategoryTheory.Pseudofunctor.comp F G : the composition of pseudofunctors

structure CategoryTheory.Pseudofunctor (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] extends CategoryTheory.PrelaxFunctor B C : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A pseudofunctor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂.

Unlike functors between categories, F.map do not need to strictly commute with the compositions, and do not need to strictly preserve the identity. Instead, there are specified 2-isomorphisms F.map (𝟙 a) ≅ 𝟙 (F.obj a) and F.map (f ≫ g) ≅ F.map f ≫ F.map g.

F.map₂ strictly commute with compositions and preserve the identity. They also preserve the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

• obj : B → C
• map {X Y : B} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (self.map f ⟶ self.map g)
• map₂_id {a b : B} (f : a ⟶ b) : self.map₂ (CategoryStruct.id f) = CategoryStruct.id (self.map f)
• map₂_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryStruct.comp η θ) = CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• mapId (a : B) : self.map (CategoryStruct.id a) ≅ CategoryStruct.id (self.obj a)
• mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : self.map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (self.map f) (self.map g)
• map₂_whisker_left {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : self.map₂ (Bicategory.whiskerLeft f η) = CategoryStruct.comp (self.mapComp f g).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f h).inv)
• map₂_whisker_right {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) : self.map₂ (Bicategory.whiskerRight η h) = CategoryStruct.comp (self.mapComp f h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map h)) (self.mapComp g h).inv)
• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : self.map₂ (Bicategory.associator f g h).hom = CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g).hom (self.map h)) (CategoryStruct.comp (Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv) (self.mapComp f (CategoryStruct.comp g h)).inv)))
• map₂_left_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).hom = CategoryStruct.comp (self.mapComp (CategoryStruct.id a) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapId a).hom (self.map f)) (Bicategory.leftUnitor (self.map f)).hom)
• map₂_right_unitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).hom = CategoryStruct.comp (self.mapComp f (CategoryStruct.id b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapId b).hom) (Bicategory.rightUnitor (self.map f)).hom)

theorem CategoryTheory.Pseudofunctor.map₂_left_unitor_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (self : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z) : CategoryStruct.comp (self.map₂ (Bicategory.leftUnitor f).hom) h = CategoryStruct.comp (self.mapComp (CategoryStruct.id a) f).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapId a).hom (self.map f)) (CategoryStruct.comp (Bicategory.leftUnitor (self.map f)).hom h))

theorem CategoryTheory.Pseudofunctor.map₂_right_unitor_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (self : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z) : CategoryStruct.comp (self.map₂ (Bicategory.rightUnitor f).hom) h = CategoryStruct.comp (self.mapComp f (CategoryStruct.id b)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapId b).hom) (CategoryStruct.comp (Bicategory.rightUnitor (self.map f)).hom h))

theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (self : Pseudofunctor B C) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) {Z : self.obj a ⟶ self.obj c} (h✝ : self.map (CategoryStruct.comp g h) ⟶ Z) : CategoryStruct.comp (self.map₂ (Bicategory.whiskerRight η h)) h✝ = CategoryStruct.comp (self.mapComp f h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map h)) (CategoryStruct.comp (self.mapComp g h).inv h✝))

theorem CategoryTheory.Pseudofunctor.map₂_associator_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (self : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : self.obj a ⟶ self.obj d} (h✝ : self.map (CategoryStruct.comp f (CategoryStruct.comp g h)) ⟶ Z) : CategoryStruct.comp (self.map₂ (Bicategory.associator f g h).hom) h✝ = CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g).hom (self.map h)) (CategoryStruct.comp (Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv) (CategoryStruct.comp (self.mapComp f (CategoryStruct.comp g h)).inv h✝))))

theorem CategoryTheory.Pseudofunctor.map₂_whisker_left_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (self : Pseudofunctor B C) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) {Z : self.obj a ⟶ self.obj c} (h✝ : self.map (CategoryStruct.comp f h) ⟶ Z) : CategoryStruct.comp (self.map₂ (Bicategory.whiskerLeft f η)) h✝ = CategoryStruct.comp (self.mapComp f g).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (CategoryStruct.comp (self.mapComp f h).inv h✝))

theorem CategoryTheory.Pseudofunctor.map₂_whisker_left_app {B : Type u_1} [Bicategory B] (self : Pseudofunctor B Cat) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)) : (self.map₂ (Bicategory.whiskerLeft f η)).app X = CategoryStruct.comp ((self.mapComp f g).hom.app X) (CategoryStruct.comp ((self.map₂ η).app ((self.map f).obj X)) ((self.mapComp f h).inv.app X))

theorem CategoryTheory.Pseudofunctor.map₂_right_unitor_app {B : Type u_1} [Bicategory B] (self : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (Bicategory.rightUnitor f).hom).app X = CategoryStruct.comp ((self.mapComp f (CategoryStruct.id b)).hom.app X) ((self.mapId b).hom.app ((self.map f).obj X))

theorem CategoryTheory.Pseudofunctor.map₂_left_unitor_app {B : Type u_1} [Bicategory B] (self : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (Bicategory.leftUnitor f).hom).app X = CategoryStruct.comp ((self.mapComp (CategoryStruct.id a) f).hom.app X) ((self.map f).map ((self.mapId a).hom.app X))

theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_app {B : Type u_1} [Bicategory B] (self : Pseudofunctor B Cat) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)) : (self.map₂ (Bicategory.whiskerRight η h)).app X = CategoryStruct.comp ((self.mapComp f h).hom.app X) (CategoryStruct.comp ((self.map h).map ((self.map₂ η).app X)) ((self.mapComp g h).inv.app X))

theorem CategoryTheory.Pseudofunctor.map₂_associator_app {B : Type u_1} [Bicategory B] (self : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : (self.map₂ (Bicategory.associator f g h).hom).app X = CategoryStruct.comp ((self.mapComp (CategoryStruct.comp f g) h).hom.app X) (CategoryStruct.comp ((self.map h).map ((self.mapComp f g).hom.app X)) (CategoryStruct.comp ((self.mapComp g h).inv.app ((self.map f).obj X)) ((self.mapComp f (CategoryStruct.comp g h)).inv.app X)))

def CategoryTheory.Pseudofunctor.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) : OplaxFunctor B C

The oplax functor associated with a pseudofunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) : F.toOplax.toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) (a : B) : F.toOplax.mapId a = (F.mapId a).hom

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toOplax.mapComp f g = (F.mapComp f g).hom

instance CategoryTheory.Pseudofunctor.hasCoeToOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : Coe (Pseudofunctor B C) (OplaxFunctor B C)

Equations

• CategoryTheory.Pseudofunctor.hasCoeToOplax = { coe := CategoryTheory.Pseudofunctor.toOplax }

def CategoryTheory.Pseudofunctor.toLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) : LaxFunctor B C

The Lax functor associated with a pseudofunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) : F.toLax.toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) (a : B) : F.toLax.mapId a = (F.mapId a).inv

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : F.toLax.mapComp f g = (F.mapComp f g).inv

instance CategoryTheory.Pseudofunctor.hasCoeToLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] : Coe (Pseudofunctor B C) (LaxFunctor B C)

Equations

• CategoryTheory.Pseudofunctor.hasCoeToLax = { coe := CategoryTheory.Pseudofunctor.toLax }

def CategoryTheory.Pseudofunctor.id (B : Type u₁) [Bicategory B] : Pseudofunctor B B

The identity pseudofunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.id_mapId (B : Type u₁) [Bicategory B] (a : B) : (id B).mapId a = Iso.refl (CategoryStruct.id a)

@[simp]

theorem CategoryTheory.Pseudofunctor.id_toPrelaxFunctor (B : Type u₁) [Bicategory B] : (id B).toPrelaxFunctor = PrelaxFunctor.id B

@[simp]

theorem CategoryTheory.Pseudofunctor.id_mapComp (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (id B).mapComp f g = Iso.refl (CategoryStruct.comp f g)

instance CategoryTheory.Pseudofunctor.instInhabited {B : Type u₁} [Bicategory B] : Inhabited (Pseudofunctor B B)

Equations

• CategoryTheory.Pseudofunctor.instInhabited = { default := CategoryTheory.Pseudofunctor.id B }

def CategoryTheory.Pseudofunctor.comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D

Composition of pseudofunctors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : Pseudofunctor B C) (G : Pseudofunctor C D) : (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.comp_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : Pseudofunctor B C) (G : Pseudofunctor C D) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (F.comp G).mapComp f g = G.map₂Iso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g)

@[simp]

theorem CategoryTheory.Pseudofunctor.comp_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {D : Type u₃} [Bicategory D] (F : Pseudofunctor B C) (G : Pseudofunctor C D) (a : B) : (F.comp G).mapId a = G.map₂Iso (F.mapId a) ≪≫ G.mapId (F.obj a)

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).hom (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) = CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).inv) (CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) (Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).hom.app X) ((F.mapComp g h).hom.app ((F.map f).obj X)) = CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).inv).app X) (CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).hom.app X) ((F.map h).map ((F.mapComp f g).hom.app X)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).obj ((F.map g).obj ((F.map f).obj X)) ⟶ Z) : CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).hom.app X) (CategoryStruct.comp ((F.mapComp g h).hom.app ((F.map f).obj X)) h✝) = CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).inv).app X) (CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).hom.app X) (CategoryStruct.comp ((F.map h).map ((F.mapComp f g).hom.app X)) h✝))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h✝ : CategoryStruct.comp (F.map f) (CategoryStruct.comp (F.map g) (F.map h)) ⟶ Z) : CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) h✝) = CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).inv) (CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).hom h✝)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).hom (Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) = CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).hom) (CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) (Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).hom.app X) ((F.map h).map ((F.mapComp f g).hom.app X)) = CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).hom).app X) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).hom.app X) ((F.mapComp g h).hom.app ((F.map f).obj X)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).obj ((F.map g).obj ((F.map f).obj X)) ⟶ Z) : CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).hom.app X) (CategoryStruct.comp ((F.map h).map ((F.mapComp f g).hom.app X)) h✝) = CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).hom).app X) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).hom.app X) (CategoryStruct.comp ((F.mapComp g h).hom.app ((F.map f).obj X)) h✝))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h✝ : CategoryStruct.comp (CategoryStruct.comp (F.map f) (F.map g)) (F.map h) ⟶ Z) : CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).hom (CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) h✝) = CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).hom) (CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).inv h✝)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (F.mapComp f (CategoryStruct.comp g h)).inv = CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).inv (CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).inv (F.map₂ (Bicategory.associator f g h).hom)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryStruct.comp ((F.mapComp g h).inv.app ((F.map f).obj X)) ((F.mapComp f (CategoryStruct.comp g h)).inv.app X) = CategoryStruct.comp ((F.map h).map ((F.mapComp f g).inv.app X)) (CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).inv.app X) ((F.map₂ (Bicategory.associator f g h).hom).app X))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryStruct.comp f (CategoryStruct.comp g h))).obj X ⟶ Z) : CategoryStruct.comp ((F.mapComp g h).inv.app ((F.map f).obj X)) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).inv.app X) h✝) = CategoryStruct.comp ((F.map h).map ((F.mapComp f g).inv.app X)) (CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).inv.app X) (CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).hom).app X) h✝))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h✝ : F.map (CategoryStruct.comp f (CategoryStruct.comp g h)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).inv h✝) = CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).inv (CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).inv (CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).hom) h✝)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (F.mapComp (CategoryStruct.comp f g) h).inv = CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).inv (F.map₂ (Bicategory.associator f g h).inv)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryStruct.comp ((F.map h).map ((F.mapComp f g).inv.app X)) ((F.mapComp (CategoryStruct.comp f g) h).inv.app X) = CategoryStruct.comp ((F.mapComp g h).inv.app ((F.map f).obj X)) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).inv.app X) ((F.map₂ (Bicategory.associator f g h).inv).app X))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d} (h✝ : F.map (CategoryStruct.comp (CategoryStruct.comp f g) h) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (CategoryStruct.comp (F.mapComp (CategoryStruct.comp f g) h).inv h✝) = CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (F.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (CategoryStruct.comp (F.mapComp f (CategoryStruct.comp g h)).inv (CategoryStruct.comp (F.map₂ (Bicategory.associator f g h).inv) h✝)))

theorem CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryStruct.comp (CategoryStruct.comp f g) h)).obj X ⟶ Z) : CategoryStruct.comp ((F.map h).map ((F.mapComp f g).inv.app X)) (CategoryStruct.comp ((F.mapComp (CategoryStruct.comp f g) h).inv.app X) h✝) = CategoryStruct.comp ((F.mapComp g h).inv.app ((F.map f).obj X)) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.comp g h)).inv.app X) (CategoryStruct.comp ((F.map₂ (Bicategory.associator f g h).inv).app X) h✝))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : (F.mapComp (CategoryStruct.id a) f).hom = CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).hom) (CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).inv (Bicategory.whiskerRight (F.mapId a).inv (F.map f)))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (F.map (CategoryStruct.id a)) (F.map f) ⟶ Z) : CategoryStruct.comp (F.mapComp (CategoryStruct.id a) f).hom h = CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).hom) (CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).inv (CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).inv (F.map f)) h))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp (CategoryStruct.id a) f).hom.app X = CategoryStruct.comp ((F.map₂ (Bicategory.leftUnitor f).hom).app X) ((F.map f).map ((F.mapId a).inv.app X))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : F.mapComp (CategoryStruct.id a) f = F.map₂Iso (Bicategory.leftUnitor f) ≪≫ (Bicategory.leftUnitor (F.map f)).symm ≪≫ (Bicategory.whiskerRightIso (F.mapId a) (F.map f)).symm

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : (F.mapComp (CategoryStruct.id a) f).inv = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (F.map f)) (CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (F.map₂ (Bicategory.leftUnitor f).inv))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map (CategoryStruct.comp (CategoryStruct.id a) f) ⟶ Z) : CategoryStruct.comp (F.mapComp (CategoryStruct.id a) f).inv h = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (F.map f)) (CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).inv) h))

theorem CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp (CategoryStruct.id a) f).inv.app X = CategoryStruct.comp ((F.map f).map ((F.mapId a).hom.app X)) ((F.map₂ (Bicategory.leftUnitor f).inv).app X)

theorem CategoryTheory.Pseudofunctor.whiskerRightIso_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (CategoryStruct.id a) f).symm ≪≫ F.map₂Iso (Bicategory.leftUnitor f) ≪≫ (Bicategory.leftUnitor (F.map f)).symm

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerRight (F.mapId a).hom (F.map f) = CategoryStruct.comp (F.mapComp (CategoryStruct.id a) f).inv (CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).hom) (Bicategory.leftUnitor (F.map f)).inv)

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (CategoryStruct.id (F.obj a)) (F.map f) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).hom (F.map f)) h = CategoryStruct.comp (F.mapComp (CategoryStruct.id a) f).inv (CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).hom) (CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).inv h))

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.map f).map ((F.mapId a).hom.app X) = CategoryStruct.comp ((F.mapComp (CategoryStruct.id a) f).inv.app X) ((F.map₂ (Bicategory.leftUnitor f).hom).app X)

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerRight (F.mapId a).inv (F.map f) = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).inv) (F.mapComp (CategoryStruct.id a) f).hom)

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (F.map (CategoryStruct.id a)) (F.map f) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a).inv (F.map f)) h = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.leftUnitor f).inv) (CategoryStruct.comp (F.mapComp (CategoryStruct.id a) f).hom h))

theorem CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.map f).map ((F.mapId a).inv.app X) = CategoryStruct.comp ((F.map₂ (Bicategory.leftUnitor f).inv).app X) ((F.mapComp (CategoryStruct.id a) f).hom.app X)

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : (F.mapComp f (CategoryStruct.id b)).hom = CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).hom) (CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).inv (Bicategory.whiskerLeft (F.map f) (F.mapId b).inv))

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (F.map f) (F.map (CategoryStruct.id b)) ⟶ Z) : CategoryStruct.comp (F.mapComp f (CategoryStruct.id b)).hom h = CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).hom) (CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).inv (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b).inv) h))

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp f (CategoryStruct.id b)).hom.app X = CategoryStruct.comp ((F.map₂ (Bicategory.rightUnitor f).hom).app X) ((F.mapId b).inv.app ((F.map f).obj X))

theorem CategoryTheory.Pseudofunctor.mapComp_id_right {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : F.mapComp f (CategoryStruct.id b) = F.map₂Iso (Bicategory.rightUnitor f) ≪≫ (Bicategory.rightUnitor (F.map f)).symm ≪≫ (Bicategory.whiskerLeftIso (F.map f) (F.mapId b)).symm

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : (F.mapComp f (CategoryStruct.id b)).inv = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b).hom) (CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (F.map₂ (Bicategory.rightUnitor f).inv))

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map (CategoryStruct.comp f (CategoryStruct.id b)) ⟶ Z) : CategoryStruct.comp (F.mapComp f (CategoryStruct.id b)).inv h = CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b).hom) (CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).inv) h))

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp f (CategoryStruct.id b)).inv.app X = CategoryStruct.comp ((F.mapId b).hom.app ((F.map f).obj X)) ((F.map₂ (Bicategory.rightUnitor f).inv).app X)

theorem CategoryTheory.Pseudofunctor.whiskerLeftIso_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerLeftIso (F.map f) (F.mapId b) = (F.mapComp f (CategoryStruct.id b)).symm ≪≫ F.map₂Iso (Bicategory.rightUnitor f) ≪≫ (Bicategory.rightUnitor (F.map f)).symm

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerLeft (F.map f) (F.mapId b).hom = CategoryStruct.comp (F.mapComp f (CategoryStruct.id b)).inv (CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).hom) (Bicategory.rightUnitor (F.map f)).inv)

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (F.map f) (CategoryStruct.id (F.obj b)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b).hom) h = CategoryStruct.comp (F.mapComp f (CategoryStruct.id b)).inv (CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).hom) (CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).inv h))

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapId b).hom.app ((F.map f).obj X) = CategoryStruct.comp ((F.mapComp f (CategoryStruct.id b)).inv.app X) ((F.map₂ (Bicategory.rightUnitor f).hom).app X)

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) : Bicategory.whiskerLeft (F.map f) (F.mapId b).inv = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).inv) (F.mapComp f (CategoryStruct.id b)).hom)

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : CategoryStruct.comp (F.map f) (F.map (CategoryStruct.id b)) ⟶ Z) : CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (F.mapId b).inv) h = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (CategoryStruct.comp (F.map₂ (Bicategory.rightUnitor f).inv) (CategoryStruct.comp (F.mapComp f (CategoryStruct.id b)).hom h))

theorem CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app {B : Type u_1} [Bicategory B] (F : Pseudofunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapId b).inv.app ((F.map f).obj X) = CategoryStruct.comp ((F.map₂ (Bicategory.rightUnitor f).inv).app X) ((F.mapComp f (CategoryStruct.id b)).hom.app X)

def CategoryTheory.Pseudofunctor.mapId' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryStruct.id b := by cat_disch) : F.map f ≅ CategoryStruct.id (F.obj b)

More flexible variant of mapId. (See the file Bicategory.Functor.Strict for applications to strict bicategories.)

Equations

• F.mapId' f hf = F.map₂Iso (CategoryTheory.eqToIso ⋯) ≪≫ F.mapId b

theorem CategoryTheory.Pseudofunctor.mapId'_eq_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) (b : B) : F.mapId' (CategoryStruct.id b) ⋯ = F.mapId b

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_mapId' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryStruct.id b := by cat_disch) : F.toLax.mapId' f hf = (F.mapId' f hf).inv

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_mapId' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryStruct.id b := by cat_disch) : F.toOplax.mapId' f hf = (F.mapId' f hf).hom

def CategoryTheory.Pseudofunctor.mapComp' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (h : CategoryStruct.comp f g = fg := by cat_disch) : F.map fg ≅ CategoryStruct.comp (F.map f) (F.map g)

More flexible variant of mapComp. (See Bicategory.Functor.Strict for applications to strict bicategories.)

Equations

• F.mapComp' f g fg h = F.map₂Iso (CategoryTheory.eqToIso ⋯) ≪≫ F.mapComp f g

theorem CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) : F.mapComp' f g (CategoryStruct.comp f g) ⋯ = F.mapComp f g

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_mapComp' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (h : CategoryStruct.comp f g = fg := by cat_disch) : F.toLax.mapComp' f g fg h = (F.mapComp' f g fg h).inv

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_mapComp' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (h : CategoryStruct.comp f g = fg := by cat_disch) : F.toOplax.mapComp' f g fg h = (F.mapComp' f g fg h).hom

def CategoryTheory.Pseudofunctor.mkOfOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C

Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (F' : F.PseudoCore) (a : B) : (mkOfOplax F F').mapId a = F'.mapIdIso a

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (F' : F.PseudoCore) : (mkOfOplax F F').toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (F' : F.PseudoCore) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (mkOfOplax F F').mapComp f g = F'.mapCompIso f g

noncomputable def CategoryTheory.Pseudofunctor.mkOfOplax' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : Pseudofunctor B C

Construct a pseudofunctor from an oplax functor whose mapId and mapComp are isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] (a : B) : ((mkOfOplax' F).mapId a).hom = F.mapId a

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] (a : B) : ((mkOfOplax' F).mapId a).inv = inv (F.mapId a)

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((mkOfOplax' F).mapComp f g).hom = F.mapComp f g

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((mkOfOplax' F).mapComp f g).inv = inv (F.mapComp f g)

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : (mkOfOplax' F).toPrelaxFunctor = F.toPrelaxFunctor

def CategoryTheory.Pseudofunctor.mkOfLax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C

Construct a pseudofunctor from a lax functor whose mapId and mapComp are isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (F' : F.PseudoCore) : (mkOfLax F F').toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax_mapComp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (F' : F.PseudoCore) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (mkOfLax F F').mapComp f g = F'.mapCompIso f g

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax_mapId {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) (F' : F.PseudoCore) (a : B) : (mkOfLax F F').mapId a = F'.mapIdIso a

noncomputable def CategoryTheory.Pseudofunctor.mkOfLax' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : Pseudofunctor B C

Construct a pseudofunctor from a lax functor whose mapId and mapComp are isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapId_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] (a : B) : ((mkOfLax' F).mapId a).hom = inv (F.mapId a)

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((mkOfLax' F).mapComp f g).hom = inv (F.mapComp f g)

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax'_toPrelaxFunctor {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] : (mkOfLax' F).toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapComp_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((mkOfLax' F).mapComp f g).inv = F.mapComp f g

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfLax'_mapId_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : LaxFunctor B C) [∀ (a : B), IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)] (a : B) : ((mkOfLax' F).mapId a).inv = F.mapId a