{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      (D : Type u_4) →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (F : CategoryTheory.Functor A B) →
                  (G : CategoryTheory.Functor B C) →
                    CategoryTheory.Join.mapPair (F.comp G) (CategoryTheory.Functor.id D) ≅
                      (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id D)).comp
                        (CategoryTheory.Join.mapPair G (CategoryTheory.Functor.id D))