{N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            AddGroupExtension N E G →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → AddGroupExtension N E' G → Type (max u_2 u_4)