Sort u →
  {k : Type u_1} →
    {V1 : Type u_2} →
      {P1 : Type u_3} →
        {V2 : Type u_4} →
          {P2 : Type u_5} →
            [inst : Ring k] →
              [inst_1 : AddCommGroup V1] →
                [inst_2 : Module k V1] →
                  [inst_3 : AddTorsor V1 P1] →
                    [inst_4 : AddCommGroup V2] →
                      [inst_5 : Module k V2] →
                        [inst_6 : AddTorsor V2 P2] →
                          (P1 →ᵃ[k] P2) →
                            {k' : Type u_1} →
                              {V1' : Type u_2} →
                                {P1' : Type u_3} →
                                  {V2' : Type u_4} →
                                    {P2' : Type u_5} →
                                      [inst' : Ring k'] →
                                        [inst'_1 : AddCommGroup V1'] →
                                          [inst'_2 : Module k' V1'] →
                                            [inst'_3 : AddTorsor V1' P1'] →
                                              [inst'_4 : AddCommGroup V2'] →
                                                [inst'_5 : Module k' V2'] →
                                                  [inst'_6 : AddTorsor V2' P2'] → (P1' →ᵃ[k'] P2') → Sort u