2-Yoneda embedding

In this file we define the bicategorical Yoneda embedding.

def CategoryTheory.Bicategory.precomposingCat {B : Type u} [Bicategory B] (a b c : B) : Functor (a ⟶ b) (Cat.of (b ⟶ c) ⟶ Cat.of (a ⟶ c))

Version of Bicategory.precomposing viewed in the bicategory Cat.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.precomposingCat_obj {B : Type u} [Bicategory B] (a b c : B) (f : a ⟶ b) : (precomposingCat a b c).obj f = (precomp c f).toCatHom

@[simp]

theorem CategoryTheory.Bicategory.precomposingCat_map {B : Type u} [Bicategory B] (a b c : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) : (precomposingCat a b c).map η = NatTrans.toCatHom₂ ((precomposing a b c).map η)

def CategoryTheory.Bicategory.postcomposingCat {B : Type u} [Bicategory B] (a b c : B) : Functor (b ⟶ c) (Cat.of (a ⟶ b) ⟶ Cat.of (a ⟶ c))

Version of Bicategory.postcomposing viewed in the bicategory Cat.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.postcomposingCat_map {B : Type u} [Bicategory B] (a b c : B) {X✝ Y✝ : b ⟶ c} (η : X✝ ⟶ Y✝) : (postcomposingCat a b c).map η = NatTrans.toCatHom₂ ((postcomposing a b c).map η)

@[simp]

theorem CategoryTheory.Bicategory.postcomposingCat_obj {B : Type u} [Bicategory B] (a b c : B) (f : b ⟶ c) : (postcomposingCat a b c).obj f = (postcomp a f).toCatHom

def CategoryTheory.Bicategory.leftUnitorNatIsoCat {B : Type u} [Bicategory B] (a b : B) : (precomposingCat a a b).obj (CategoryStruct.id a) ≅ CategoryStruct.id (Cat.of (a ⟶ b))

Left unitor as a 2-isomorphism in Cat.

Equations

• CategoryTheory.Bicategory.leftUnitorNatIsoCat a b = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.NatIso.ofComponents (fun (x : a ⟶ b) => CategoryTheory.Bicategory.leftUnitor x) ⋯)

@[simp]

theorem CategoryTheory.Bicategory.leftUnitorNatIsoCat_hom_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (X : a ⟶ b) : (leftUnitorNatIsoCat a b).hom.toNatTrans.app X = (leftUnitor X).hom

@[simp]

theorem CategoryTheory.Bicategory.leftUnitorNatIsoCat_inv_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (X : a ⟶ b) : (leftUnitorNatIsoCat a b).inv.toNatTrans.app X = (leftUnitor X).inv

def CategoryTheory.Bicategory.associatorNatIsoRightCat {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) : (precomposingCat a c d).obj (CategoryStruct.comp f g) ≅ CategoryStruct.comp ((precomposingCat b c d).obj g) ((precomposingCat a b d).obj f)

Right component of the associator as a 2-isomorphism in Cat.

Equations

• CategoryTheory.Bicategory.associatorNatIsoRightCat f g d = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.NatIso.ofComponents (fun (x : c ⟶ d) => CategoryTheory.Bicategory.associator f g x) ⋯)

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoRightCat_hom_toNatTrans_app {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (associatorNatIsoRightCat f g d).hom.toNatTrans.app X = (associator f g X).hom

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoRightCat_inv_toNatTrans_app {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (associatorNatIsoRightCat f g d).inv.toNatTrans.app X = (associator f g X).inv

def CategoryTheory.Bicategory.associatorNatIsoMiddleCat {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) : CategoryStruct.comp ((precomposingCat a b c).obj f) ((postcomposingCat a c d).obj h) ≅ CategoryStruct.comp ((postcomposingCat b c d).obj h) ((precomposingCat a b d).obj f)

Middle component of the associator as a 2-isomorphism in Cat.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoMiddleCat_hom_toNatTrans_app {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : ↑(Cat.of (b ⟶ c))) : (associatorNatIsoMiddleCat f h).hom.toNatTrans.app X = (associator f X h).hom

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoMiddleCat_inv_toNatTrans_app {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : ↑(Cat.of (b ⟶ c))) : (associatorNatIsoMiddleCat f h).inv.toNatTrans.app X = (associator f X h).inv

def CategoryTheory.Bicategory.rightUnitorNatIsoCat {B : Type u} [Bicategory B] (a b : B) : (postcomposingCat a b b).obj (CategoryStruct.id b) ≅ CategoryStruct.id (Cat.of (a ⟶ b))

Right unitor as a 2-isomorphism in Cat.

Equations

• CategoryTheory.Bicategory.rightUnitorNatIsoCat a b = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.NatIso.ofComponents (fun (x : a ⟶ b) => CategoryTheory.Bicategory.rightUnitor x) ⋯)

@[simp]

theorem CategoryTheory.Bicategory.rightUnitorNatIsoCat_inv_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (X : a ⟶ b) : (rightUnitorNatIsoCat a b).inv.toNatTrans.app X = (rightUnitor X).inv

@[simp]

theorem CategoryTheory.Bicategory.rightUnitorNatIsoCat_hom_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (X : a ⟶ b) : (rightUnitorNatIsoCat a b).hom.toNatTrans.app X = (rightUnitor X).hom

def CategoryTheory.Bicategory.associatorNatIsoLeftCat {B : Type u} [Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp ((postcomposingCat a b c).obj g) ((postcomposingCat a c d).obj h) ≅ (postcomposingCat a b d).obj (CategoryStruct.comp g h)

Left component of the associator as a 2-isomorphism in Cat.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoLeftCat_hom_toNatTrans_app {B : Type u} [Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) (X : ↑(Cat.of (a ⟶ b))) : (associatorNatIsoLeftCat a g h).hom.toNatTrans.app X = (associator X g h).hom

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoLeftCat_inv_toNatTrans_app {B : Type u} [Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) (X : ↑(Cat.of (a ⟶ b))) : (associatorNatIsoLeftCat a g h).inv.toNatTrans.app X = (associator X g h).inv

def CategoryTheory.Bicategory.yoneda₀ {B : Type u} [Bicategory B] (x : B) : Pseudofunctor Bᵒᵖ Cat

The map on objects underlying the Yoneda embedding. It sends an object x to the pseudofunctor defined by:

• Objects: a ↦ (a ⟶ x)
• Higher morphisms get sent to the corresponding "precomposing" operation.

This is only used for defining yoneda, after which Bicategory.yoneda.obj should be prefered.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α {B : Type u} [Bicategory B] (x : B) (y : Bᵒᵖ) : ↑((yoneda₀ x).obj y) = (Opposite.unop y ⟶ x)

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_mapComp_inv_toNatTrans_app {B : Type u} [Bicategory B] (x : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x) : ((yoneda₀ x).mapComp f g).inv.toNatTrans.app X = (associator g.unop f.unop X).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj {B : Type u} [Bicategory B] (x : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) (x✝ : Opposite.unop a ⟶ x) : ((yoneda₀ x).map a✝).toFunctor.obj x✝ = CategoryStruct.comp a✝.unop x✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_mapId_hom_toNatTrans_app {B : Type u} [Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x) : ((yoneda₀ x).mapId a).hom.toNatTrans.app X = (leftUnitor X).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_mapComp_hom_toNatTrans_app {B : Type u} [Bicategory B] (x : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x) : ((yoneda₀ x).mapComp f g).hom.toNatTrans.app X = (associator g.unop f.unop X).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_mapId_inv_toNatTrans_app {B : Type u} [Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x) : ((yoneda₀ x).mapId a).inv.toNatTrans.app X = (leftUnitor X).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app {B : Type u} [Bicategory B] (x : B) {a b : Bᵒᵖ} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x✝ : Opposite.unop a ⟶ x) : ((yoneda₀ x).map₂ a✝).toNatTrans.app x✝ = whiskerRight a✝.unop2 x✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map {B : Type u} [Bicategory B] (x : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) {X✝ Y✝ : Opposite.unop a ⟶ x} (x✝ : X✝ ⟶ Y✝) : ((yoneda₀ x).map a✝).toFunctor.map x✝ = whiskerLeft a✝.unop x✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str {B : Type u} [Bicategory B] (x : B) (y : Bᵒᵖ) : ((yoneda₀ x).obj y).str = homCategory (Opposite.unop y) x

def CategoryTheory.Bicategory.postcomp₂ {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) : yoneda₀ a ⟶ yoneda₀ b

Postcomposing of a 1-morphism seen as a strong transformation between pseudofunctors.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.postcomp₂_app_toFunctor_map {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : ((postcomp₂ f).app x).toFunctor.map x✝ = whiskerRight x✝ f

@[simp]

theorem CategoryTheory.Bicategory.postcomp₂_naturality_hom_toNatTrans_app {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝ ⟶ a))) : ((postcomp₂ f).naturality g).hom.toNatTrans.app X = (associator g.unop X f).hom

@[simp]

theorem CategoryTheory.Bicategory.postcomp₂_naturality_inv_toNatTrans_app {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝ ⟶ a))) : ((postcomp₂ f).naturality g).inv.toNatTrans.app X = (associator g.unop X f).inv

@[simp]

theorem CategoryTheory.Bicategory.postcomp₂_app_toFunctor_obj {B : Type u} [Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((postcomp₂ f).app x).toFunctor.obj x✝ = CategoryStruct.comp x✝ f

def CategoryTheory.Bicategory.postcomposing₂ {B : Type u} [Bicategory B] (a b : B) : Functor (a ⟶ b) (yoneda₀ a ⟶ yoneda₀ b)

Postcomposing of 1-morphisms seen as a functor from a ⟶ b to the hom-category of the corresponding pseudofunctors.

This is an implementation detail, and Bicategory.yoneda.map should be prefered.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.postcomposing₂_obj_naturality_hom_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝ ⟶ a))) : (((postcomposing₂ a b).obj f).naturality g).hom.toNatTrans.app X = (associator g.unop X f).hom

@[simp]

theorem CategoryTheory.Bicategory.postcomposing₂_map_as_app_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : (((postcomposing₂ a b).map η).as.app x).toNatTrans.app x✝ = whiskerLeft x✝ η

@[simp]

theorem CategoryTheory.Bicategory.postcomposing₂_obj_naturality_inv_toNatTrans_app {B : Type u} [Bicategory B] (a b : B) (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝ ⟶ a))) : (((postcomposing₂ a b).obj f).naturality g).inv.toNatTrans.app X = (associator g.unop X f).inv

@[simp]

theorem CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_map {B : Type u} [Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : (((postcomposing₂ a b).obj f).app x).toFunctor.map x✝ = whiskerRight x✝ f

@[simp]

theorem CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_obj {B : Type u} [Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : (((postcomposing₂ a b).obj f).app x).toFunctor.obj x✝ = CategoryStruct.comp x✝ f

def CategoryTheory.Bicategory.yoneda {B : Type u} [Bicategory B] : Pseudofunctor B (Pseudofunctor Bᵒᵖ Cat)

The Yoneda pseudofunctor from B to Bᵒᵖ ⥤ᵖ Cat.

It consists of the following:

• On objects: sends x : B to the pseudofunctor Bᵒᵖ ⥤ᵖ Cat given by a ↦ (a ⟶ x) on objects and on 1- and 2-morphisms given by "precomposing"
• On 1- and 2-morphisms it is given by "postcomposing"

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str {B : Type u} [Bicategory B] (x✝ : B) (y : Bᵒᵖ) : ((yoneda.obj x✝).obj y).str = homCategory (Opposite.unop y) x✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda_mapId_inv_as_app_toNatTrans_app {B : Type u} [Bicategory B] (a : B) (a✝ : Bᵒᵖ) (X : Opposite.unop a✝ ⟶ a) : ((yoneda.mapId a).inv.as.app a✝).toNatTrans.app X = (rightUnitor X).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app {B : Type u} [Bicategory B] {a b : B} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((yoneda.map₂ a✝).as.app x).toNatTrans.app x✝ = whiskerLeft x✝ a✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app {B : Type u} [Bicategory B] (x✝ : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x✝) : ((yoneda.obj x✝).mapComp f g).inv.toNatTrans.app X = (associator g.unop f.unop X).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda_mapId_hom_as_app_toNatTrans_app {B : Type u} [Bicategory B] (a : B) (a✝ : Bᵒᵖ) (X : Opposite.unop a✝ ⟶ a) : ((yoneda.mapId a).hom.as.app a✝).toNatTrans.app X = (rightUnitor X).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app {B : Type u} [Bicategory B] (x✝ : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x✝) : ((yoneda.obj x✝).mapId a).hom.toNatTrans.app X = (leftUnitor X).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj {B : Type u} [Bicategory B] {a b : B} (a✝ : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((yoneda.map a✝).app x).toFunctor.obj x✝ = CategoryStruct.comp x✝ a✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app {B : Type u} [Bicategory B] (x✝ : B) {a b : Bᵒᵖ} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x✝¹ : Opposite.unop a ⟶ x✝) : ((yoneda.obj x✝).map₂ a✝).toNatTrans.app x✝¹ = whiskerRight a✝.unop2 x✝¹

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app {B : Type u} [Bicategory B] (x✝ : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x✝) : ((yoneda.obj x✝).mapId a).inv.toNatTrans.app X = (leftUnitor X).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α {B : Type u} [Bicategory B] (x✝ : B) (y : Bᵒᵖ) : ↑((yoneda.obj x✝).obj y) = (Opposite.unop y ⟶ x✝)

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map {B : Type u} [Bicategory B] {a b : B} (a✝ : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : ((yoneda.map a✝).app x).toFunctor.map x✝ = whiskerRight x✝ a✝

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj {B : Type u} [Bicategory B] (x✝ : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) (x✝¹ : Opposite.unop a ⟶ x✝) : ((yoneda.obj x✝).map a✝).toFunctor.obj x✝¹ = CategoryStruct.comp a✝.unop x✝¹

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app {B : Type u} [Bicategory B] {a b : B} (a✝ : a ⟶ b) {a✝¹ b✝ : Bᵒᵖ} (g : a✝¹ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝¹ ⟶ a))) : ((yoneda.map a✝).naturality g).inv.toNatTrans.app X = (associator g.unop X a✝).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app {B : Type u} [Bicategory B] (x✝ : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x✝) : ((yoneda.obj x✝).mapComp f g).hom.toNatTrans.app X = (associator g.unop f.unop X).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda_mapComp_inv_as_app_toNatTrans_app {B : Type u} [Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (a : Bᵒᵖ) (X : ↑(Cat.of (Opposite.unop a ⟶ a✝))) : ((yoneda.mapComp f g).inv.as.app a).toNatTrans.app X = (associator X f g).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app {B : Type u} [Bicategory B] {a b : B} (a✝ : a ⟶ b) {a✝¹ b✝ : Bᵒᵖ} (g : a✝¹ ⟶ b✝) (X : ↑(Cat.of (Opposite.unop a✝¹ ⟶ a))) : ((yoneda.map a✝).naturality g).hom.toNatTrans.app X = (associator g.unop X a✝).hom

@[simp]

theorem CategoryTheory.Bicategory.yoneda_mapComp_hom_as_app_toNatTrans_app {B : Type u} [Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (a : Bᵒᵖ) (X : ↑(Cat.of (Opposite.unop a ⟶ a✝))) : ((yoneda.mapComp f g).hom.as.app a).toNatTrans.app X = (associator X f g).inv

@[simp]

theorem CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map {B : Type u} [Bicategory B] (x✝ : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) {X✝ Y✝ : Opposite.unop a ⟶ x✝} (x✝¹ : X✝ ⟶ Y✝) : ((yoneda.obj x✝).map a✝).toFunctor.map x✝¹ = whiskerLeft a✝.unop x✝¹