# Oplax functors #

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.

## Main definitions #

• CategoryTheory.OplaxFunctor B C : an oplax functor between bicategories B and C
• CategoryTheory.OplaxFunctor.comp F G : the composition of oplax functors
structure CategoryTheory.OplaxFunctor (B : Type u₁) (C : Type u₂) extends :
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.

Instances For
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {f : a b} {f' : a b} (η : f f') (g : b c) :
CategoryTheory.CategoryStruct.comp (self.map₂ ) (self.mapComp f' g) = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map g))
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_right {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} (f : a b) {g : b c} {g' : b c} (η : g g') :
CategoryTheory.CategoryStruct.comp (self.map₂ ) (self.mapComp f g') = CategoryTheory.CategoryStruct.comp (self.mapComp f g) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η))
@[simp]
theorem CategoryTheory.OplaxFunctor.map₂_associator {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) :
CategoryTheory.CategoryStruct.comp (self.map₂ .hom) (CategoryTheory.CategoryStruct.comp (self.mapComp f ) (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) = CategoryTheory.CategoryStruct.comp (self.mapComp 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)
@[simp]
theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) :
@[simp]
theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) :
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_left_assoc {B : Type u₁} {C : Type u₂} (self : ) {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) :
@[simp]
theorem CategoryTheory.OplaxFunctor.map₂_associator_assoc {B : Type u₁} {C : Type u₂} (self : ) {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) :
@[simp]
theorem CategoryTheory.OplaxFunctor.mapComp_naturality_right_assoc {B : Type u₁} {C : Type u₂} (self : ) {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) :
theorem CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : self.obj a self.obj b} (h : self.map f Z) :
theorem CategoryTheory.OplaxFunctor.map₂_rightUnitor_assoc {B : Type u₁} {C : Type u₂} (self : ) {a : B} {b : B} (f : a b) {Z : self.obj a self.obj b} (h : self.map f Z) :
@[simp]
theorem CategoryTheory.OplaxFunctor.id_toPrelaxFunctor (B : Type u₁) :
.toPrelaxFunctor =
@[simp]
theorem CategoryTheory.OplaxFunctor.id_mapId (B : Type u₁) (a : B) :
@[simp]
theorem CategoryTheory.OplaxFunctor.id_mapComp (B : Type u₁) :
∀ {a b c : B} (f : a b) (g : b c),

The identity oplax functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• CategoryTheory.OplaxFunctor.instInhabited = { default := }
def CategoryTheory.OplaxFunctor.comp {B : Type u₁} {C : Type u₂} {D : Type u₃} (F : ) (G : ) :

Composition of oplax functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
structure CategoryTheory.OplaxFunctor.PseudoCore {B : Type u₁} {C : Type u₂} (F : ) :
Type (max (max u₁ v₁) w₂)

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

Instances For
@[simp]
theorem CategoryTheory.OplaxFunctor.PseudoCore.mapIdIso_hom {B : Type u₁} {C : Type u₂} {F : } (self : F.PseudoCore) {a : B} :
(self.mapIdIso a).hom = F.mapId a
@[simp]
theorem CategoryTheory.OplaxFunctor.PseudoCore.mapCompIso_hom {B : Type u₁} {C : Type u₂} {F : } (self : F.PseudoCore) {a : B} {b : B} {c : B} (f : a b) (g : b c) :
(self.mapCompIso f g).hom = F.mapComp f g