Sort u →
  {ι : Type u_1} →
    {G : ι → Type u_2} →
      {H : Type u_3} →
        [inst : (i : ι) → Group (G i)] →
          [inst_1 : Group H] →
            {φ : (i : ι) → H →* G i} →
              {d : Monoid.PushoutI.NormalWord.Transversal φ} →
                {i : ι} →
                  Monoid.PushoutI.NormalWord.Pair d i →
                    {ι' : Type u_1} →
                      {G' : ι' → Type u_2} →
                        {H' : Type u_3} →
                          [inst' : (i : ι') → Group (G' i)] →
                            [inst'_1 : Group H'] →
                              {φ' : (i : ι') → H' →* G' i} →
                                {d' : Monoid.PushoutI.NormalWord.Transversal φ'} →
                                  {i' : ι'} → Monoid.PushoutI.NormalWord.Pair d' i' → Sort u