Strong natural transformations #

A strong natural transformation is an oplax natural transformation such that each component 2-cell is an isomorphism.

Main definitions #

StrongOplaxNatTrans F G : strong natural transformations between oplax functors F and G.
mkOfOplax η η' : given an oplax natural transformation η such that each component 2-cell is an isomorphism, mkOfOplax gives the corresponding strong natural transformation.
StrongOplaxNatTrans.vcomp η θ : the vertical composition of strong natural transformations η and θ.
StrongOplaxNatTrans.category F G : a category structure on pseudofunctors between F and G, where the morphisms are strong natural transformations.

TODO #

After having defined lax functors, we should define 3 different types of strong natural transformations:

strong natural transformations between oplax functors (as defined here).
strong natural transformations between lax functors.
strong natural transformations between pseudofunctors. From these types of strong natural transformations, we can define the underlying natural transformations between the underlying oplax resp. lax functors. Many properties can then be inferred from these.

References #

Niles Johnson, Donald Yau, 2-Dimensional Categories

source

structure CategoryTheory.StrongOplaxNatTrans {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F G : OplaxFunctor B C) :

Type (max (max (max u₁ v₁) v₂) w₂)

A strong natural transformation between oplax functors F and G is a natural transformation that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:

a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B.
a 2-isomorphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b.
These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

app (a : B) : F.obj a ⟶ G.obj a
naturality {a b : B} (f : a ⟶ b) : CategoryStruct.comp (F.map f) (self.app b) ≅ CategoryStruct.comp (self.app a) (G.map f)
naturality_naturality {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g).hom = CategoryStruct.comp (self.naturality f).hom (Bicategory.whiskerLeft (self.app a) (G.map₂ η))
naturality_id (a : B) : CategoryStruct.comp (self.naturality (CategoryStruct.id a)).hom (Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (Bicategory.rightUnitor (self.app a)).inv)
naturality_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryStruct.comp (self.naturality (CategoryStruct.comp f g)).hom (Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryStruct.comp (Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (F.map f) (self.naturality g).hom) (CategoryStruct.comp (Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryStruct.comp (Bicategory.whiskerRight (self.naturality f).hom (G.map g)) (Bicategory.associator (self.app a) (G.map f) (G.map g)).hom))))

Instances For

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongOplaxNatTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a} (h : CategoryStruct.comp (self.app a) (CategoryStruct.id (G.obj a)) ⟶ Z) :

CategoryStruct.comp (self.naturality (CategoryStruct.id a)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.mapId a)) h) = CategoryStruct.comp (Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryStruct.comp (Bicategory.leftUnitor (self.app a)).hom (CategoryStruct.comp (Bicategory.rightUnitor (self.app a)).inv h))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongOplaxNatTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c} (h : CategoryStruct.comp (self.app a) (CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z) :

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (self : StrongOplaxNatTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) {Z : F.obj a ⟶ G.obj b} (h : CategoryStruct.comp (self.app a) (G.map g) ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerRight (F.map₂ η) (self.app b)) (CategoryStruct.comp (self.naturality g).hom h) = CategoryStruct.comp (self.naturality f).hom (CategoryStruct.comp (Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)

source

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

OplaxNatTrans F G

The underlying oplax natural transformation of a strong natural transformation.

Equations

η.toOplax = { app := η.app, naturality := fun {a b : B} (f : a ⟶ b) => (η.naturality f).hom, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.toOplax_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a✝ b✝ : B} (f : a✝ ⟶ b✝) :

η.toOplax.naturality f = (η.naturality f).hom

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.toOplax_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) (a : B) :

η.toOplax.app a = η.app a

source

def CategoryTheory.StrongOplaxNatTrans.mkOfOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans F G) (η' : η.StrongCore) :

StrongOplaxNatTrans F G

Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.

Equations

CategoryTheory.StrongOplaxNatTrans.mkOfOplax η η' = { app := η.app, naturality := fun {a b : B} => η'.naturality, naturality_naturality := ⋯, naturality_id := ⋯, naturality_comp := ⋯ }

Instances For

source

noncomputable def CategoryTheory.StrongOplaxNatTrans.mkOfOplax' {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : OplaxNatTrans F G) [∀ (a b : B) (f : a ⟶ b), IsIso (η.naturality f)] :

StrongOplaxNatTrans F G

Construct a strong natural transformation from an oplax natural transformation whose naturality 2-cell is an isomorphism.

Equations

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

Instances For

source

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

StrongOplaxNatTrans F F

The identity strong natural transformation.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) (a : B) :

(id F).app a = CategoryStruct.id (F.obj a)

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) :

((id F).naturality f).hom = CategoryStruct.comp (Bicategory.rightUnitor (F.map f)).hom (Bicategory.leftUnitor (F.map f)).inv

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) {a✝ b✝ : B} (f : a✝ ⟶ b✝) :

((id F).naturality f).inv = CategoryStruct.comp (Bicategory.leftUnitor (F.map f)).hom (Bicategory.rightUnitor (F.map f)).inv

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.id.toOplax {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) :

(id F).toOplax = OplaxNatTrans.id F

source

instance CategoryTheory.StrongOplaxNatTrans.instInhabited {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] (F : OplaxFunctor B C) :

Inhabited (StrongOplaxNatTrans F F)

Equations

CategoryTheory.StrongOplaxNatTrans.instInhabited F = { default := CategoryTheory.StrongOplaxNatTrans.id F }

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) :

CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (Bicategory.whiskerLeft f (θ.naturality h).hom) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) {Z : a' ⟶ H.obj b} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (H.map h)) ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality h).hom) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality g).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.map₂ β))) h✝)

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_naturality {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') :

CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (Bicategory.whiskerRight (η.naturality g).hom h) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (Bicategory.associator (η.app a) (G.map g) h).inv))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_naturality_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a b : B} {a' : C} {f g : a ⟶ b} (β : f ⟶ g) (h : G.obj b ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality g).hom h) h✝) = CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom h) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map f) h).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.map₂ β) h)) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map g) h).inv h✝)))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) {Z : a' ⟶ H.obj c} (h✝ : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.comp (H.map g) (H.map h))) ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.comp g h)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) h✝) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom)) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (θ.naturality g).hom (H.map h))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom) h✝)))))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_comp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') :

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_comp_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') {Z : F.obj a ⟶ a'} (h✝ : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.comp (G.map f) (G.map g)) h) ⟶ Z) :

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) :

CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a)).hom) (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerLeft_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {G H : OplaxFunctor B C} (θ : StrongOplaxNatTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a) {Z : a' ⟶ H.obj a} (h : CategoryStruct.comp f (CategoryStruct.comp (θ.app a) (CategoryStruct.id (H.obj a))) ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerLeft f (θ.naturality (CategoryStruct.id a)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerLeft (θ.app a) (H.mapId a))) h) = CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.leftUnitor (θ.app a)).hom) (CategoryStruct.comp (Bicategory.whiskerLeft f (Bicategory.rightUnitor (θ.app a)).inv) h))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_id {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') :

CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)).hom f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f))) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.whiskerRight_naturality_id_assoc {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) {a : B} {a' : C} (f : G.obj a ⟶ a') {Z : F.obj a ⟶ a'} (h : CategoryStruct.comp (η.app a) (CategoryStruct.comp (CategoryStruct.id (G.obj a)) f) ⟶ Z) :

CategoryStruct.comp (Bicategory.whiskerRight (η.naturality (CategoryStruct.id a)).hom f) (CategoryStruct.comp (Bicategory.associator (η.app a) (G.map (CategoryStruct.id a)) f).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a) (Bicategory.whiskerRight (G.mapId a) f)) h)) = CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.leftUnitor (η.app a)).hom f) (CategoryStruct.comp (Bicategory.whiskerRight (Bicategory.rightUnitor (η.app a)).inv f) (CategoryStruct.comp (Bicategory.associator (η.app a) (CategoryStruct.id (G.obj a)) f).hom h)))

source

def CategoryTheory.StrongOplaxNatTrans.vcomp {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) (θ : StrongOplaxNatTrans G H) :

StrongOplaxNatTrans F H

Vertical composition of strong natural transformations.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.vcomp_naturality_inv {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) (θ : StrongOplaxNatTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) :

((η.vcomp θ).naturality f).inv = CategoryStruct.comp (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).inv) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).inv (θ.app b✝)) (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).hom)))

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.vcomp_app {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) (θ : StrongOplaxNatTrans G H) (a : B) :

(η.vcomp θ).app a = CategoryStruct.comp (η.app a) (θ.app a)

source

@[simp]

theorem CategoryTheory.StrongOplaxNatTrans.vcomp_naturality_hom {B : Type u₁} [Bicategory B] {C : Type u₂} [Bicategory C] {F G H : OplaxFunctor B C} (η : StrongOplaxNatTrans F G) (θ : StrongOplaxNatTrans G H) {a✝ b✝ : B} (f : a✝ ⟶ b✝) :

((η.vcomp θ).naturality f).hom = CategoryStruct.comp (Bicategory.associator (F.map f) (η.app b✝) (θ.app b✝)).inv (CategoryStruct.comp (Bicategory.whiskerRight (η.naturality f).hom (θ.app b✝)) (CategoryStruct.comp (Bicategory.associator (η.app a✝) (G.map f) (θ.app b✝)).hom (CategoryStruct.comp (Bicategory.whiskerLeft (η.app a✝) (θ.naturality f).hom) (Bicategory.associator (η.app a✝) (θ.app a✝) (H.map f)).inv)))

source

instance CategoryTheory.Pseudofunctor.categoryStruct (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :

CategoryStruct.{max (max (max u₁ v₂) v₁) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁} (Pseudofunctor B C)

Equations

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

source

@[simp]

theorem CategoryTheory.Pseudofunctor.categoryStruct_id (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (F : Pseudofunctor B C) :

CategoryStruct.id F = StrongOplaxNatTrans.id F.toOplax

source

@[simp]

theorem CategoryTheory.Pseudofunctor.categoryStruct_comp (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : Pseudofunctor B C} (η : StrongOplaxNatTrans X✝.toOplax Y✝.toOplax) (θ : StrongOplaxNatTrans Y✝.toOplax Z✝.toOplax) :

CategoryStruct.comp η θ = η.vcomp θ

Documentation

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong

Strong natural transformations #

Main definitions #

TODO #

References #