∀ (D : Type u_3) [inst : CategoryTheory.Category.{u_4, u_3} D] {a b : CategoryTheory.Cat} (f : a ⟶ b),
  CategoryTheory.NatTrans.toCatHom₂
      (CategoryTheory.Join.mapWhiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom.toNatTrans
        (CategoryTheory.Functor.id D)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Cat.Hom.isoMk
          (CategoryTheory.Join.mapCompLeft D f.toFunctor (CategoryTheory.CategoryStruct.id b).toFunctor)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft
          (CategoryTheory.Join.mapPair f.toFunctor (CategoryTheory.Functor.id D)).toCatHom
          (CategoryTheory.Cat.Hom.isoMk CategoryTheory.Join.mapPairId).hom)
        (CategoryTheory.Bicategory.rightUnitor
            (CategoryTheory.Join.mapPair f.toFunctor (CategoryTheory.Functor.id D)).toCatHom).hom)