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₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor , CategoryTheory.PrelaxFunctorStruct , Prefunctor : 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₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
• map₂_comp : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h), self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• mapId : (a : B) → self.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (self.obj a)
• mapComp : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → self.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.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₂ (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.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₂ (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.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₂ (CategoryTheory.Bicategory.associator f g h).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom (self.map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))
• map₂_left_unitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
• map₂_right_unitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b).hom) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem CategoryTheory.Pseudofunctor.map₂_whisker_right_app {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)).app X = CategoryTheory.CategoryStruct.comp ((self.mapComp f h).hom.app X) (CategoryTheory.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} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).app X = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).map ((self.mapComp f g).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.app ((self.map f).obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.app X))))

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

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

def CategoryTheory.Pseudofunctor.toOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : CategoryTheory.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_mapId {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) : F.toOplax.mapId a = (F.mapId a).hom

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.toOplax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] : Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.OplaxFunctor B C)

Equations

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

def CategoryTheory.Pseudofunctor.toLax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) : F.toLax.toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.toLax_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] : Coe (CategoryTheory.Pseudofunctor B C) (CategoryTheory.LaxFunctor B C)

Equations

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

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

The identity pseudofunctor.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

def CategoryTheory.Pseudofunctor.comp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D) : (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.comp_mapComp {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] {D : Type u₃} [CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_hom_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : F.obj a ⟶ 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)).hom h = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv) h))

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

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

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

theorem CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {a : B} {b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).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 (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv) h))

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

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

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

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

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

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

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

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

def CategoryTheory.Pseudofunctor.mkOfOplax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) : CategoryTheory.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_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (F' : F.PseudoCore) : (CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Pseudofunctor.mkOfOplax' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] : CategoryTheory.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'_toPrelaxFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] : (CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Pseudofunctor.mkOfLax {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) : CategoryTheory.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₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) (F' : F.PseudoCore) : (CategoryTheory.Pseudofunctor.mkOfLax F F').toPrelaxFunctor = F.toPrelaxFunctor

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Pseudofunctor.mkOfLax' {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] : CategoryTheory.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'_mapComp_hom {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.LaxFunctor B C) [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).hom = CategoryTheory.inv (F.mapComp f g)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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