{I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      {c₁ : ComplexShape I₁} →
        {c₂ : ComplexShape I₂} →
          {c₁₂ : ComplexShape I₁₂} →
            {P : Sort u} →
              {π : I₁ × I₂ → I₁₂} →
                {ε₁ ε₂ : I₁ × I₂ → ℤˣ} →
                  {rel₁ : ∀ {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.Rel (π (i₁, i₂)) (π (i₁', i₂))} →
                    {rel₂ : ∀ (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → c₁₂.Rel (π (i₁, i₂)) (π (i₁, i₂'))} →
                      {ε₂_ε₁ :
                          ∀ {i₁ i₁' : I₁} {i₂ i₂' : I₂},
                            c₁.Rel i₁ i₁' → c₂.Rel i₂ i₂' → ε₂ (i₁, i₂) * ε₁ (i₁, i₂') = -ε₁ (i₁, i₂) * ε₂ (i₁', i₂)} →
                        {π' : I₁ × I₂ → I₁₂} →
                          {ε₁' ε₂' : I₁ × I₂ → ℤˣ} →
                            {rel₁' :
                                ∀ {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), c₁₂.Rel (π' (i₁, i₂)) (π' (i₁', i₂))} →
                              {rel₂' :
                                  ∀ (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → c₁₂.Rel (π' (i₁, i₂)) (π' (i₁, i₂'))} →
                                {ε₂_ε₁' :
                                    ∀ {i₁ i₁' : I₁} {i₂ i₂' : I₂},
                                      c₁.Rel i₁ i₁' →
                                        c₂.Rel i₂ i₂' → ε₂' (i₁, i₂) * ε₁' (i₁, i₂') = -ε₁' (i₁, i₂) * ε₂' (i₁', i₂)} →
                                  { π := π, ε₁ := ε₁, ε₂ := ε₂, rel₁ := rel₁, rel₂ := rel₂, ε₂_ε₁ := ε₂_ε₁ } =
                                      { π := π', ε₁ := ε₁', ε₂ := ε₂', rel₁ := rel₁', rel₂ := rel₂', ε₂_ε₁ := ε₂_ε₁' } →
                                    (π ≍ π' → ε₁ ≍ ε₁' → ε₂ ≍ ε₂' → P) → P