Isomorphisms and coherence in Cat #
A 2-morphism in Cat is invertible if all its components are invertible. The associator and
right unitor of identity functors in the bicategory of categories are identity natural
transformations.
theorem
CategoryTheory.Cat.Hom₂.isIso_of_isIso_app
{C D : Cat}
{F G : C ⟶ D}
(α : F ⟶ G)
[∀ (X : ↑C), IsIso (α.toNatTrans.app X)]
:
IsIso α
A 2-morphism in Cat is invertible if all its components are invertible.
@[simp]
theorem
CategoryTheory.Cat.associator_id_hom
(C : Type w)
[Category.{v, w} C]
:
(Bicategory.associator (CategoryStruct.id ↧C) (CategoryStruct.id ↧C) (CategoryStruct.id ↧C)).hom = CategoryStruct.id
(CategoryStruct.comp (CategoryStruct.comp (CategoryStruct.id ↧C) (CategoryStruct.id ↧C)) (CategoryStruct.id ↧C))
The associator of three identity functors in Cat is the identity.
@[simp]
theorem
CategoryTheory.Cat.associator_id_inv
(C : Type w)
[Category.{v, w} C]
:
(Bicategory.associator (CategoryStruct.id ↧C) (CategoryStruct.id ↧C) (CategoryStruct.id ↧C)).inv = CategoryStruct.id
(CategoryStruct.comp (CategoryStruct.id ↧C) (CategoryStruct.comp (CategoryStruct.id ↧C) (CategoryStruct.id ↧C)))
The inverse associator of three identity functors in Cat is the identity.
@[simp]
The right unitor of the identity functor in Cat is the identity.
@[simp]
The inverse right unitor of the identity functor in Cat is the identity.