Oplax functors and pseudofunctors

An oplax functor F between bicategories B and C consists of

• a function between objects F.obj : B ⟶ C,
• a family of functions between 1-morphisms F.map : (a ⟶ b) → (F.obj a ⟶ F.obj b),
• a family of functions between 2-morphisms F.map₂ : (f ⟶ g) → (F.map f ⟶ F.map g),
• a family of 2-morphisms F.mapId a : F.map (𝟙 a) ⟶ 𝟙 (F.obj a),
• a family of 2-morphisms F.mapComp f g : F.map (f ≫ g) ⟶ F.map f ≫ F.map g, and
• certain consistency conditions on them.

A pseudofunctor is an oplax 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.

The additional constructors are useful when constructing a pseudofunctor where the construction of the oplax functor associated with it is already done. For example, the composition of pseudofunctors can be defined by using the composition of oplax functors as follows:

def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D :=
  mkOfOplax ((F : OplaxFunctor B C).comp G)
  { mapIdIso := fun a ↦ (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
    mapCompIso := fun f g ↦
      (G.mapFunctor _ _).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g) }

although the composition of pseudofunctors in this file is defined by using the default constructor because obviously wasn't smart enough in mathlib3 and the porter of this file was too lazy to investigate this issue further in mathlib4. Similarly, the composition is also defined by using mkOfOplax' after giving appropriate instances for IsIso. The former constructor mkOfOplax requires isomorphisms as data type Iso, and so it is useful if you don't want to forget the definitions of the inverses. On the other hand, the latter constructor mkOfOplax' is useful if you want to use propositional type class IsIso.

Main definitions

• CategoryTheory.OplaxFunctor B C : an oplax functor between bicategories B and C
• CategoryTheory.OplaxFunctor.comp F G : the composition of oplax functors
• CategoryTheory.Pseudofunctor B C : a pseudofunctor between bicategories B and C
• CategoryTheory.Pseudofunctor.comp F G : the composition of pseudofunctors

Future work

There are two types of functors between bicategories, called lax and oplax functors, depending on the directions of mapId and mapComp. We may need both in mathlib in the future, but for now we only define oplax functors.

structure CategoryTheory.PrelaxFunctor (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] (C : Type u₂) [Quiver C] [(a b : C) → Quiver (a ⟶ b)] extends Prefunctor : Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A prelax functor between bicategories consists of functions between objects, 1-morphisms, and 2-morphisms. This structure will be extended to define OplaxFunctor.

• 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)

  The action of a prelax functor on 2-morphisms.

instance CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] : Coe (CategoryTheory.PrelaxFunctor B C) (B ⥤q C)

Equations

• CategoryTheory.PrelaxFunctor.hasCoeToPrefunctor = { coe := CategoryTheory.PrelaxFunctor.toPrefunctor }

@[simp]

theorem CategoryTheory.PrelaxFunctor.id_map₂ (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (CategoryTheory.PrelaxFunctor.id B).map₂ η = η

@[simp]

theorem CategoryTheory.PrelaxFunctor.id_toPrefunctor (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] : ↑(CategoryTheory.PrelaxFunctor.id B) = 𝟭q B

def CategoryTheory.PrelaxFunctor.id (B : Type u₁) [Quiver B] [(a b : B) → Quiver (a ⟶ b)] : CategoryTheory.PrelaxFunctor B B

The identity prelax functor.

Equations

• CategoryTheory.PrelaxFunctor.id B = let __src := 𝟭q B; { toPrefunctor := __src, map₂ := fun {a b : B} {f g : a ⟶ b} (η : f ⟶ g) => η }

instance CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] : Inhabited (CategoryTheory.PrelaxFunctor B B)

Equations

• CategoryTheory.PrelaxFunctor.instInhabitedPrelaxFunctor = { default := CategoryTheory.PrelaxFunctor.id B }

@[simp]

theorem CategoryTheory.PrelaxFunctor.comp_toPrefunctor {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) : ↑(CategoryTheory.PrelaxFunctor.comp F G) = ↑F ⋙q ↑G

@[simp]

theorem CategoryTheory.PrelaxFunctor.comp_map₂ {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (CategoryTheory.PrelaxFunctor.comp F G).map₂ η = G.map₂ (F.map₂ η)

def CategoryTheory.PrelaxFunctor.comp {B : Type u₁} [Quiver B] [(a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [Quiver C] [(a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [Quiver D] [(a b : D) → Quiver (a ⟶ b)] (F : CategoryTheory.PrelaxFunctor B C) (G : CategoryTheory.PrelaxFunctor C D) : CategoryTheory.PrelaxFunctor B D

Composition of prelax functors.

Equations

• CategoryTheory.PrelaxFunctor.comp F G = let __src := ↑F ⋙q ↑G; { toPrefunctor := __src, map₂ := fun {a b : B} {f g : a ⟶ b} (η : f ⟶ g) => G.map₂ (F.map₂ η) }

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

An oplax functor 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 composition, and do not need to strictly preserve the identity. Instead, there are specified 2-morphisms 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)
• 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)
• mapComp_naturality_left : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
• mapComp_naturality_right : ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)) (self.mapComp f g') = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
• 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₂ θ)
• map₂_associator : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom)
• map₂_leftUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
• map₂_rightUnitor : ∀ {a b : B} (f : a ⟶ b), self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)

@[simp]

theorem CategoryTheory.OplaxFunctor.map₂_associator_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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 : CategoryTheory.CategoryStruct.comp (self.map f) (CategoryTheory.CategoryStruct.comp (self.map g) (self.map h✝)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h✝).hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h✝)) h)) = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h✝)).hom h))

@[simp]

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

@[simp]

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

theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom h))

theorem CategoryTheory.OplaxFunctor.map₂_comp_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor B C) {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h✝) {Z : self.obj a ⟶ self.obj b} (h : self.map h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (self.map₂ η) (CategoryTheory.CategoryStruct.comp (self.map₂ θ) h)

theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (self : CategoryTheory.OplaxFunctor 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) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom h))

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

Equations

• CategoryTheory.OplaxFunctor.hasCoeToPrelax = { coe := CategoryTheory.OplaxFunctor.toPrelaxFunctor }

@[simp]

theorem CategoryTheory.OplaxFunctor.mapFunctor_obj {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) (f : a ⟶ b) : (CategoryTheory.OplaxFunctor.mapFunctor F a b).obj f = F.map f

@[simp]

theorem CategoryTheory.OplaxFunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) : ∀ {X Y : a ⟶ b} (η : X ⟶ Y), (CategoryTheory.OplaxFunctor.mapFunctor F a b).map η = F.map₂ η

def CategoryTheory.OplaxFunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) (a : B) (b : B) : CategoryTheory.Functor (a ⟶ b) (F.obj a ⟶ F.obj b)

Function between 1-morphisms as a functor.

Equations

• CategoryTheory.OplaxFunctor.mapFunctor F a b = { toPrefunctor := { obj := fun (f : a ⟶ b) => F.map f, map := fun {X Y : a ⟶ b} (η : X ⟶ Y) => F.map₂ η }, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity oplax functor.

Equations

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

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

Equations

• CategoryTheory.OplaxFunctor.instInhabitedOplaxFunctor = { default := CategoryTheory.OplaxFunctor.id B }

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

Composition of oplax functors.

Equations

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

structure CategoryTheory.OplaxFunctor.PseudoCore {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) : Type (max (max u₁ v₁) w₂)

A structure on an oplax functor that promotes an oplax functor to a pseudofunctor. See Pseudofunctor.mkOfOplax.

• mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)
• mapCompIso : {a b c : B} → (f : a ⟶ b) → (g : b ⟶ c) → F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)
• mapIdIso_hom : ∀ {a : B}, (self.mapIdIso a).hom = F.mapId a
• mapCompIso_hom : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (self.mapCompIso f g).hom = F.mapComp f g

structure CategoryTheory.Pseudofunctor (B : Type u₁) [CategoryTheory.Bicategory B] (C : Type u₂) [CategoryTheory.Bicategory C] extends CategoryTheory.PrelaxFunctor : 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)
• 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₂_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₂ θ)
• 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)

theorem CategoryTheory.Pseudofunctor.map₂_comp_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} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h✝) {Z : self.obj a ⟶ self.obj b} (h : self.map h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (self.map₂ η) (CategoryTheory.CategoryStruct.comp (self.map₂ θ) 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₂_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_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₂_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₂_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))

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

Equations

• CategoryTheory.Pseudofunctor.hasCoeToPrelaxFunctor = { coe := CategoryTheory.Pseudofunctor.toPrelaxFunctor }

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.

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 }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Pseudofunctor.mapFunctor_map {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) : ∀ {X Y : a ⟶ b} (η : X ⟶ Y), (CategoryTheory.Pseudofunctor.mapFunctor F a b).map η = (CategoryTheory.Pseudofunctor.toOplax F).map₂ η

@[simp]

theorem CategoryTheory.Pseudofunctor.mapFunctor_obj {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.Pseudofunctor.mapFunctor F a b).obj f = (CategoryTheory.Pseudofunctor.toOplax F).map f

def CategoryTheory.Pseudofunctor.mapFunctor {B : Type u₁} [CategoryTheory.Bicategory B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) (a : B) (b : B) : CategoryTheory.Functor (a ⟶ b) (F.obj a ⟶ F.obj b)

Function on 1-morphisms as a functor.

Equations

• CategoryTheory.Pseudofunctor.mapFunctor F a b = CategoryTheory.OplaxFunctor.mapFunctor (CategoryTheory.Pseudofunctor.toOplax F) a b

@[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_mapId (B : Type u₁) [CategoryTheory.Bicategory B] (a : B) : (CategoryTheory.Pseudofunctor.id B).mapId a = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id a)

@[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)

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.

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

Equations

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

@[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), (CategoryTheory.Pseudofunctor.comp F G).mapComp f g = (CategoryTheory.Pseudofunctor.mapFunctor G (F.obj a) (F.obj c)).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g)

@[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) : (CategoryTheory.Pseudofunctor.comp F G).mapId a = (CategoryTheory.Pseudofunctor.mapFunctor G (F.obj a) (F.obj a)).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a)

@[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) : (CategoryTheory.Pseudofunctor.comp F G).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.comp F.toPrelaxFunctor G.toPrelaxFunctor

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp {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 = CategoryTheory.asIso (F.mapComp f g)

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.