Pseudofunctors to Cat

In this file, we state naturality properties of mapId' and mapComp' for pseudofunctors to Cat.

theorem CategoryTheory.Pseudofunctor.mapId'_hom_naturality {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryStruct.id b₀) (a : X ⟶ Y) : CategoryStruct.comp ((F.map f).map a) ((F.mapId' f hf).hom.app Y) = CategoryStruct.comp ((F.mapId' f hf).hom.app X) a

theorem CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryStruct.id b₀) (a : X ⟶ Y) {Z : ↑(F.obj b₀)} (h : (CategoryStruct.id (F.obj b₀)).obj Y ⟶ Z) : CategoryStruct.comp ((F.map f).map a) (CategoryStruct.comp ((F.mapId' f hf).hom.app Y) h) = CategoryStruct.comp ((F.mapId' f hf).hom.app X) (CategoryStruct.comp a h)

theorem CategoryTheory.Pseudofunctor.mapId'_inv_naturality {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryStruct.id b₀) (a : X ⟶ Y) : CategoryStruct.comp ((F.mapId' f hf).inv.app X) ((F.map f).map a) = CategoryStruct.comp a ((F.mapId' f hf).inv.app Y)

theorem CategoryTheory.Pseudofunctor.mapId'_inv_naturality_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryStruct.id b₀) (a : X ⟶ Y) {Z : ↑(F.obj b₀)} (h : (F.map f).obj Y ⟶ Z) : CategoryStruct.comp ((F.mapId' f hf).inv.app X) (CategoryStruct.comp ((F.map f).map a) h) = CategoryStruct.comp a (CategoryStruct.comp ((F.mapId' f hf).inv.app Y) h)

theorem CategoryTheory.Pseudofunctor.mapComp'_hom_naturality {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) : CategoryStruct.comp ((F.map fg).map a) ((F.mapComp' f g fg hfg).hom.app Y) = CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app X) ((F.map g).map ((F.map f).map a))

theorem CategoryTheory.Pseudofunctor.mapComp'_hom_naturality_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)} (h : (CategoryStruct.comp (F.map f) (F.map g)).obj Y ⟶ Z) : CategoryStruct.comp ((F.map fg).map a) (CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app Y) h) = CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app X) (CategoryStruct.comp ((F.map g).map ((F.map f).map a)) h)

theorem CategoryTheory.Pseudofunctor.mapComp'_inv_naturality {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) : CategoryStruct.comp ((F.map g).map ((F.map f).map a)) ((F.mapComp' f g fg hfg).inv.app Y) = CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app X) ((F.map fg).map a)

theorem CategoryTheory.Pseudofunctor.mapComp'_inv_naturality_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)} (h : (F.map fg).obj Y ⟶ Z) : CategoryStruct.comp ((F.map g).map ((F.map f).map a)) (CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app Y) h) = CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app X) (CategoryStruct.comp ((F.map fg).map a) h)

theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_1 {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) : CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app X) (CategoryStruct.comp ((F.map fg).map a) ((F.mapComp' f g fg hfg).hom.app Y)) = (F.map g).map ((F.map f).map a)

theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_1_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)} (h : (CategoryStruct.comp (F.map f) (F.map g)).obj Y ⟶ Z) : CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app X) (CategoryStruct.comp ((F.map fg).map a) (CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app Y) h)) = CategoryStruct.comp ((F.map g).map ((F.map f).map a)) h

theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_2 {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) : CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app X) (CategoryStruct.comp ((F.map g).map ((F.map f).map a)) ((F.mapComp' f g fg hfg).inv.app Y)) = (F.map fg).map a

theorem CategoryTheory.Pseudofunctor.mapComp'_naturality_2_assoc {B : Type u} [Bicategory B] (F : Pseudofunctor B Cat) {b₀ b₁ b₂ : B} {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂) (hfg : CategoryStruct.comp f g = fg) (a : X ⟶ Y) {Z : ↑(F.obj b₂)} (h : (F.map fg).obj Y ⟶ Z) : CategoryStruct.comp ((F.mapComp' f g fg hfg).hom.app X) (CategoryStruct.comp ((F.map g).map ((F.map f).map a)) (CategoryStruct.comp ((F.mapComp' f g fg hfg).inv.app Y) h)) = CategoryStruct.comp ((F.map fg).map a) h