{ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} → Monoid.PushoutI.NormalWord.Transversal φ → Type (max (max u_1 u_2) u_3)