-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- Constructor for morphisms from
`(mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j`.  -/
HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₂₃ : Type u_4} →
      {C₃ : Type u_5} →
        {C₄ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] →
                    [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                      [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                        [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃] →
                          [inst_8 : CategoryTheory.Preadditive C₂₃] →
                            [inst_9 : CategoryTheory.Preadditive C₄] →
                              {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} →
                                {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} →
                                  [inst_10 : G₂₃.PreservesZeroMorphisms] →
                                    [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] →
                                      [inst_12 : F.PreservesZeroMorphisms] →
                                        [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                          {ι₁ : Type u_7} →
                                            {ι₂ : Type u_8} →
                                              {ι₃ : Type u_9} →
                                                {ι₁₂ : Type u_10} →
                                                  {ι₂₃ : Type u_11} →
                                                    {ι₄ : Type u_12} →
                                                      [inst_14 : DecidableEq ι₄] →
                                                        {c₁ : ComplexShape ι₁} →
                                                          {c₂ : ComplexShape ι₂} →
                                                            {c₃ : ComplexShape ι₃} →
                                                              {K₁ : HomologicalComplex C₁ c₁} →
                                                                {K₂ : HomologicalComplex C₂ c₂} →
                                                                  {K₃ : HomologicalComplex C₃ c₃} →
                                                                    (c₁₂ : ComplexShape ι₁₂) →
                                                                      {c₂₃ : ComplexShape ι₂₃} →
                                                                        {c₄ : ComplexShape ι₄} →
                                                                          [inst_15 : TotalComplexShape c₁ c₂ c₁₂] →
                                                                            [inst_16 : TotalComplexShape c₁₂ c₃ c₄] →
                                                                              [inst_17 : TotalComplexShape c₂ c₃ c₂₃] →
                                                                                [inst_18 :
                                                                                    TotalComplexShape c₁ c₂₃ c₄] →
                                                                                  [inst_19 :
                                                                                      K₂.HasMapBifunctor K₃ G₂₃ c₂₃] →
                                                                                    [inst_20 :
                                                                                        c₁.Associative c₂ c₃ c₁₂ c₂₃
                                                                                          c₄] →
                                                                                      [inst_21 : DecidableEq ι₂₃] →
                                                                                        [inst_22 :
                                                                                            K₁.HasMapBifunctor
                                                                                              (K₂.mapBifunctor K₃ G₂₃
                                                                                                c₂₃)
                                                                                              F c₄] →
                                                                                          [HomologicalComplex.HasGoodTrifunctor₂₃Obj
                                                                                                F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃
                                                                                                c₄] →
                                                                                            {j : ι₄} →
                                                                                              {A : C₄} →
                                                                                                ((i₁ : ι₁) →
                                                                                                    (i₂ : ι₂) → ⋯) →
                                                                                                  (⋯.X j ⟶ A)