Lax functors

A lax 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.obj a) ⟶ F.map (𝟙 a),
• a family of 2-morphisms F.mapComp f g : F.map f ≫ F.map g ⟶ F.map (f ≫ g), and
• certain consistency conditions on them.

Main definitions

• CategoryTheory.LaxFunctor B C : a lax functor between bicategories B and C, which we denote by B ⥤ᴸ C.
• CategoryTheory.LaxFunctor.comp F G : the composition of lax functors
• CategoryTheory.LaxFunctor.Pseudocore : a structure on a Lax functor that promotes a Lax functor to a pseudofunctor

Future work

Some constructions in the bicategory library have only been done in terms of oplax functors, since lax functors had not yet been added (e.g FunctorBicategory.lean). A possible project would be to mirror these constructions for lax functors.

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

A lax 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.obj a) ⟶ F.map (𝟙 a) and F.map f ≫ F.map g ⟶ F.map (f ≫ g).

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

• obj : B → C
• map {X Y : B} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (self.map f ⟶ self.map g)
• map₂_id {a b : B} (f : a ⟶ b) : self.map₂ (CategoryStruct.id f) = CategoryStruct.id (self.map f)
• map₂_comp {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : self.map₂ (CategoryStruct.comp η θ) = CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
• mapId (a : B) : CategoryStruct.id (self.obj a) ⟶ self.map (CategoryStruct.id a)

  The 2-morphism underlying the lax unity constraint.

• mapComp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.map f) (self.map g) ⟶ self.map (CategoryStruct.comp f g)

  The 2-morphism underlying the lax functoriality constraint.

• mapComp_naturality_left {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerRight η g)) = CategoryStruct.comp (Bicategory.whiskerRight (self.map₂ η) (self.map g)) (self.mapComp f' g)

  Naturality of the lax functoriality constraint, on the left.

• mapComp_naturality_right {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') : CategoryStruct.comp (self.mapComp f g) (self.map₂ (Bicategory.whiskerLeft f η)) = CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f g')

  Naturality of the lax functoriality constraint, on the right.

• map₂_associator {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (Bicategory.whiskerRight (self.mapComp f g) (self.map h)) (CategoryStruct.comp (self.mapComp (CategoryStruct.comp f g) h) (self.map₂ (Bicategory.associator f g h).hom)) = CategoryStruct.comp (Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapComp g h)) (self.mapComp f (CategoryStruct.comp g h)))

  Lax associativity.

• map₂_leftUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.leftUnitor f).inv = CategoryStruct.comp (Bicategory.leftUnitor (self.map f)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.mapId a) (self.map f)) (self.mapComp (CategoryStruct.id a) f))

  Lax left unity.

• map₂_rightUnitor {a b : B} (f : a ⟶ b) : self.map₂ (Bicategory.rightUnitor f).inv = CategoryStruct.comp (Bicategory.rightUnitor (self.map f)).inv (CategoryStruct.comp (Bicategory.whiskerLeft (self.map f) (self.mapId b)) (self.mapComp f (CategoryStruct.id b)))

  Lax right unity.

def CategoryTheory.Bicategory.«term_⥤ᴸ_» : Lean.TrailingParserDescr

Notation for a lax functor between bicategories.

Equations

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

@[simp]

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

Lax associativity.

@[simp]

theorem CategoryTheory.LaxFunctor.mapComp_naturality_left_app {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) : CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map₂ (Bicategory.whiskerRight η g)).toNatTrans.app X) = CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) ((self.mapComp f' g).toNatTrans.app X)

Naturality of the lax functoriality constraint, on the left.

@[simp]

theorem CategoryTheory.LaxFunctor.mapComp_naturality_right_app {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) : CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X) = CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f g').toNatTrans.app X)

Naturality of the lax functoriality constraint, on the right.

@[simp]

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

Lax associativity.

@[simp]

theorem CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map (CategoryStruct.comp f' g)).toFunctor.obj X ⟶ Z) : CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryStruct.comp ((self.map₂ (Bicategory.whiskerRight η g)).toNatTrans.app X) h) = CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) (CategoryStruct.comp ((self.mapComp f' g).toNatTrans.app X) h)

Naturality of the lax functoriality constraint, on the left.

@[simp]

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

Naturality of the lax functoriality constraint, on the left.

@[simp]

theorem CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map (CategoryStruct.comp f g')).toFunctor.obj X ⟶ Z) : CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryStruct.comp ((self.map₂ (Bicategory.whiskerLeft f η)).toNatTrans.app X) h) = CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryStruct.comp ((self.mapComp f g').toNatTrans.app X) h)

Naturality of the lax functoriality constraint, on the right.

@[simp]

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

Naturality of the lax functoriality constraint, on the right.

@[simp]

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

Lax associativity.

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

Lax right unity.

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

Lax left unity.

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map (CategoryStruct.comp f (CategoryStruct.id b))).toFunctor.obj X ⟶ Z) : CategoryStruct.comp ((self.map₂ (Bicategory.rightUnitor f).inv).toNatTrans.app X) h = CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryStruct.comp ((self.mapComp f (CategoryStruct.id b)).toNatTrans.app X) h)

Lax right unity.

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

Lax left unity.

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

Lax right unity.

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc {B : Type u_1} [Bicategory B] (self : LaxFunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map (CategoryStruct.comp (CategoryStruct.id a) f)).toFunctor.obj X ⟶ Z) : CategoryStruct.comp ((self.map₂ (Bicategory.leftUnitor f).inv).toNatTrans.app X) h = CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X)) (CategoryStruct.comp ((self.mapComp (CategoryStruct.id a) f).toNatTrans.app X) h)

Lax left unity.

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc {B : Type u_1} [Bicategory B] (F : LaxFunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map f).toFunctor.obj ((CategoryStruct.id (F.obj a)).toFunctor.obj X) ⟶ Z) : h = CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).toNatTrans.app X)) (CategoryStruct.comp ((F.mapComp (CategoryStruct.id a) f).toNatTrans.app X) (CategoryStruct.comp ((F.map₂ (Bicategory.leftUnitor f).hom).toNatTrans.app X) h))

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

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

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

theorem CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc {B : Type u_1} [Bicategory B] (F : LaxFunctor B Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : h = CategoryStruct.comp ((F.mapId b).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryStruct.comp ((F.mapComp f (CategoryStruct.id b)).toNatTrans.app X) (CategoryStruct.comp ((F.map₂ (Bicategory.rightUnitor f).hom).toNatTrans.app X) h))

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

The identity lax functor.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

Equations

• F.mapId' f hf = CategoryTheory.CategoryStruct.comp (F.mapId b) (F.map₂ (CategoryTheory.eqToHom ⋯))

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

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

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

Equations

• F.mapComp' f g fg h = CategoryTheory.CategoryStruct.comp (F.mapComp f g) (F.map₂ (CategoryTheory.eqToHom ⋯))

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

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

Composition of lax functors.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A structure on a Lax functor that promotes a Lax functor to a pseudofunctor.

See Pseudofunctor.mkOfLax.

• mapIdIso (a : B) : F.map (CategoryStruct.id a) ≅ CategoryStruct.id (F.obj a)

  The isomorphism giving rise to the lax unity constraint

• mapCompIso {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : F.map (CategoryStruct.comp f g) ≅ CategoryStruct.comp (F.map f) (F.map g)

  The isomorphism giving rise to the lax functoriality constraint

• mapIdIso_inv {a : B} : (self.mapIdIso a).inv = F.mapId a

  mapIdIso gives rise to the lax unity constraint

• mapCompIso_inv {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : (self.mapCompIso f g).inv = F.mapComp f g

  mapCompIso gives rise to the lax functoriality constraint