eqToHom in bicategories

This file records some of the behavior of eqToHom 1-morphisms and 2-morphisms in bicategories.

Given an equality of objects h : x = y in a bicategory, there is a 1-morphism eqToHom h : x ⟶ y just like in an ordinary category. The definitional property of this morphism is that if h : x = x, eqToHom h = 𝟙 x. This is implemented as the eqToHom morphism in the CategoryStruct underlying the bicategory.

Unlike the situation in ordinary category theory, these 1-morphisms do not compose strictly: eqToHom h.trans h' is merely isomorphic to eqToHom h ≫ eqToHom h'. We define this isomorphism as CategoryTheory.Bicategory.eqToHomTransIso.

Given an equality of 1-morphisms, we show that various bicategorical structure morphisms such as unitors, associators and whiskering conjugate well under eqToHoms.

TODO

• Define eqToEquiv that puts the eqToHoms in an Equivalence between objects.

def CategoryTheory.Bicategory.eqToHomTransIso {B : Type u} [Bicategory B] {x y z : B} (e₁ : x = y) (e₂ : y = z) : eqToHom ⋯ ≅ CategoryStruct.comp (eqToHom e₁) (eqToHom e₂)

In a bicategory, eqToHoms do not compose strictly, but they do up to isomorphism.

@[simp]

theorem CategoryTheory.Bicategory.eqToHomTransIso_refl_refl {B : Type u} [Bicategory B] (x : B) : eqToHomTransIso ⋯ ⋯ = (leftUnitor (CategoryStruct.id x)).symm

theorem CategoryTheory.Bicategory.eqToHomTransIso_refl_right {B : Type u} [Bicategory B] {x y : B} (e₁ : x = y) : eqToHomTransIso e₁ ⋯ = (rightUnitor (eqToHom e₁)).symm

theorem CategoryTheory.Bicategory.eqToHomTransIso_refl_left {B : Type u} [Bicategory B] {x y : B} (e₁ : x = y) : eqToHomTransIso ⋯ e₁ = (leftUnitor (eqToHom e₁)).symm

theorem CategoryTheory.Bicategory.associator_eqToHom_hom {B : Type u} [Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) : (associator (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).hom = CategoryStruct.comp (whiskerRight (eqToHomTransIso e₁ e₂).inv (eqToHom e₃)) (CategoryStruct.comp (eqToHomTransIso ⋯ e₃).inv (CategoryStruct.comp (eqToHomTransIso e₁ ⋯).hom (whiskerLeft (eqToHom e₁) (eqToHomTransIso e₂ e₃).hom)))

theorem CategoryTheory.Bicategory.associator_eqToHom_hom_assoc {B : Type u} [Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) {Z : x ⟶ t} (h : CategoryStruct.comp (eqToHom e₁) (CategoryStruct.comp (eqToHom e₂) (eqToHom e₃)) ⟶ Z) : CategoryStruct.comp (associator (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).hom h = CategoryStruct.comp (whiskerRight (eqToHomTransIso e₁ e₂).inv (eqToHom e₃)) (CategoryStruct.comp (eqToHomTransIso ⋯ e₃).inv (CategoryStruct.comp (eqToHomTransIso e₁ ⋯).hom (CategoryStruct.comp (whiskerLeft (eqToHom e₁) (eqToHomTransIso e₂ e₃).hom) h)))

theorem CategoryTheory.Bicategory.associator_eqToHom_inv {B : Type u} [Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) : (associator (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).inv = CategoryStruct.comp (whiskerLeft (eqToHom e₁) (eqToHomTransIso e₂ e₃).inv) (CategoryStruct.comp (eqToHomTransIso e₁ ⋯).inv (CategoryStruct.comp (eqToHomTransIso ⋯ e₃).hom (whiskerRight (eqToHomTransIso e₁ e₂).hom (eqToHom e₃))))

theorem CategoryTheory.Bicategory.associator_eqToHom_inv_assoc {B : Type u} [Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) {Z : x ⟶ t} (h : CategoryStruct.comp (CategoryStruct.comp (eqToHom e₁) (eqToHom e₂)) (eqToHom e₃) ⟶ Z) : CategoryStruct.comp (associator (eqToHom e₁) (eqToHom e₂) (eqToHom e₃)).inv h = CategoryStruct.comp (whiskerLeft (eqToHom e₁) (eqToHomTransIso e₂ e₃).inv) (CategoryStruct.comp (eqToHomTransIso e₁ ⋯).inv (CategoryStruct.comp (eqToHomTransIso ⋯ e₃).hom (CategoryStruct.comp (whiskerRight (eqToHomTransIso e₁ e₂).hom (eqToHom e₃)) h)))

theorem CategoryTheory.Bicategory.associator_hom_congr {B : Type u} [Bicategory B] {x y z t : B} {f f' : x ⟶ y} {g g' : y ⟶ z} {h h' : z ⟶ t} (ef : f = f') (eg : g = g') (eh : h = h') : (associator f g h).hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (associator f' g' h').hom (eqToHom ⋯))

theorem CategoryTheory.Bicategory.associator_inv_congr {B : Type u} [Bicategory B] {x y z t : B} {f f' : x ⟶ y} {g g' : y ⟶ z} {h h' : z ⟶ t} (ef : f = f') (eg : g = g') (eh : h = h') : (associator f g h).inv = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (associator f' g' h').inv (eqToHom ⋯))

theorem CategoryTheory.Bicategory.congr_whiskerLeft {B : Type u} [Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') {z : B} {g g' : y ⟶ z} (η : g ⟶ g') : whiskerLeft f η = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (whiskerLeft f' η) (eqToHom ⋯))

theorem CategoryTheory.Bicategory.whiskerRight_congr {B : Type u} [Bicategory B] {y z : B} {g g' : y ⟶ z} (h : g = g') {x : B} {f f' : x ⟶ y} (η : f ⟶ f') : whiskerRight η g = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (whiskerRight η g') (eqToHom ⋯))

theorem CategoryTheory.Bicategory.leftUnitor_hom_congr {B : Type u} [Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') : (leftUnitor f).hom = CategoryStruct.comp (whiskerLeft (CategoryStruct.id x) (eqToHom h)) (CategoryStruct.comp (leftUnitor f').hom (eqToHom ⋯))

theorem CategoryTheory.Bicategory.leftUnitor_inv_congr {B : Type u} [Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') : (leftUnitor f).inv = CategoryStruct.comp (eqToHom h) (CategoryStruct.comp (leftUnitor f').inv (whiskerLeft (CategoryStruct.id x) (eqToHom ⋯)))

theorem CategoryTheory.Bicategory.rightUnitor_hom_congr {B : Type u} [Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') : (rightUnitor f).hom = CategoryStruct.comp (whiskerRight (eqToHom h) (CategoryStruct.id y)) (CategoryStruct.comp (rightUnitor f').hom (eqToHom ⋯))

theorem CategoryTheory.Bicategory.rightUnitor_inv_congr {B : Type u} [Bicategory B] {x y : B} {f f' : x ⟶ y} (h : f = f') : (rightUnitor f).inv = CategoryStruct.comp (eqToHom h) (CategoryStruct.comp (rightUnitor f').inv (whiskerRight (eqToHom ⋯) (CategoryStruct.id y)))