Sort u →
  {𝕜 : Type u_1} →
    {V : Type u_2} →
      {V₂ : Type u_5} →
        {P : Type u_10} →
          {P₂ : Type u_11} →
            [inst : NormedField 𝕜] →
              [inst_1 : SeminormedAddCommGroup V] →
                [inst_2 : NormedSpace 𝕜 V] →
                  [inst_3 : PseudoMetricSpace P] →
                    [inst_4 : NormedAddTorsor V P] →
                      [inst_5 : SeminormedAddCommGroup V₂] →
                        [inst_6 : NormedSpace 𝕜 V₂] →
                          [inst_7 : PseudoMetricSpace P₂] →
                            [inst_8 : NormedAddTorsor V₂ P₂] →
                              (P ≃ᵃⁱ[𝕜] P₂) →
                                {𝕜' : Type u_1} →
                                  {V' : Type u_2} →
                                    {V₂' : Type u_5} →
                                      {P' : Type u_10} →
                                        {P₂' : Type u_11} →
                                          [inst' : NormedField 𝕜'] →
                                            [inst'_1 : SeminormedAddCommGroup V'] →
                                              [inst'_2 : NormedSpace 𝕜' V'] →
                                                [inst'_3 : PseudoMetricSpace P'] →
                                                  [inst'_4 : NormedAddTorsor V' P'] →
                                                    [inst'_5 : SeminormedAddCommGroup V₂'] →
                                                      [inst'_6 : NormedSpace 𝕜' V₂'] →
                                                        [inst'_7 : PseudoMetricSpace P₂'] →
                                                          [inst'_8 : NormedAddTorsor V₂' P₂'] →
                                                            (P' ≃ᵃⁱ[𝕜'] P₂') → Sort u