Sort u →
  {I₁ : Type u_1} →
    {I₂ : Type u_2} →
      {I₁₂ : Type u_4} →
        {c₁ : ComplexShape I₁} →
          {c₂ : ComplexShape I₂} →
            {c₁₂ : ComplexShape I₁₂} →
              [inst : TotalComplexShape c₁ c₂ c₁₂] →
                [inst_1 : TotalComplexShape c₂ c₁ c₁₂] →
                  TotalComplexShapeSymmetry c₁ c₂ c₁₂ →
                    {I₁' : Type u_1} →
                      {I₂' : Type u_2} →
                        {I₁₂' : Type u_4} →
                          {c₁' : ComplexShape I₁'} →
                            {c₂' : ComplexShape I₂'} →
                              {c₁₂' : ComplexShape I₁₂'} →
                                [inst' : TotalComplexShape c₁' c₂' c₁₂'] →
                                  [inst'_1 : TotalComplexShape c₂' c₁' c₁₂'] →
                                    TotalComplexShapeSymmetry c₁' c₂' c₁₂' → Sort u