diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a1c6e6b83f11..88f8bcdf7852 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -97,6 +97,7 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
       mb.mind_packets
   in
   let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in
+  let mind_entry_sort_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_sort_variance in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
@@ -104,6 +105,7 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_variance;
+    mind_entry_sort_variance;
     mind_entry_private = mb.mind_private;
   }
 
@@ -210,6 +212,7 @@ let check_inductive env mind mb =
   let { mind_packets; mind_finite; mind_hyps; mind_univ_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
         mind_universes; mind_template; mind_variance; mind_sec_variance;
+        mind_sort_variance; mind_sec_sort_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
@@ -236,6 +239,9 @@ let check_inductive env mind mb =
   check "mind_variance" (Option.equal (Array.equal UVars.Variance.equal)
                            mb.mind_variance mind_variance);
   check "mind_sec_variance" (Option.is_empty mind_sec_variance);
+  check "mind_sort_variance" (Option.equal (Array.equal UVars.Variance.equal)
+                           mb.mind_sort_variance mind_sort_variance);
+  check "mind_sec_sort_variance" (Option.is_empty mind_sec_sort_variance);
   ignore mind_private; (* passed through Indtypes *)
 
   ignore mind_typing_flags;
diff --git a/checker/values.ml b/checker/values.ml
index fbf3274d5ff2..32f431431026 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -482,6 +482,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_opt v_template_universes;
     v_opt (v_array v_variance);
     v_opt (v_array v_variance);
+    v_opt (v_array v_variance);
+    v_opt (v_array v_variance);
     v_opt v_bool;
     v_typing_flags|]
 
diff --git a/doc/changelog/01-kernel/21770-sort-cumulativity-Added.rst b/doc/changelog/01-kernel/21770-sort-cumulativity-Added.rst
new file mode 100644
index 000000000000..f3a57c80b08a
--- /dev/null
+++ b/doc/changelog/01-kernel/21770-sort-cumulativity-Added.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  :flag:`Polymorphic Inductive Sort Cumulativity` to allow sorts in the same
+  connected component ({Prop, Type/Set} or {SProp}) to be treated as equivalent
+  at quality positions with non-Invariant inferred variance in cumulative inductives
+  (`#21770 <https://github.com/rocq-prover/rocq/pull/21770>`_,
+  by Jason Gross).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 0d14c1259ee1..c8a191407ee0 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -433,6 +433,27 @@ Insufficiently restrictive variance annotations lead to errors:
           Defined.
       End down.
 
+Sort Cumulativity
+~~~~~~~~~~~~~~~~~
+
+.. flag:: Polymorphic Inductive Sort Cumulativity
+
+   When this :term:`flag` is on (it is off by default), it enables sort
+   cumulativity for cumulative polymorphic inductive types. This means that
+   sort/quality positions with non-Invariant inferred variance allow sorts in
+   the same connected component to be treated as equivalent. The connected
+   components are:
+
+   - ``{Prop, Type/Set}`` (both "relevant" sorts)
+   - ``{SProp}`` (alone)
+
+   For example, with sort cumulativity enabled, a cumulative polymorphic
+   inductive ``Iso@{s s'; u u'}`` declared at ``Iso@{Prop Prop; Set Set}``
+   can be used where ``Iso@{Type Prop; Set Set}`` is expected, because
+   ``Prop`` and ``Type`` are in the same connected component.
+
+   This flag requires :flag:`Polymorphic Inductive Cumulativity` to be on.
+
 Cumulativity Weak Constraints
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f31e880d4529..3a63a87a1a07 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -757,7 +757,8 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
   | Some variances ->
     let num_param_arity = Conversion.inductive_cumulativity_arguments spec in
     if not (Int.equal num_param_arity nargs) then enforce_eq_instances_univs false u1 u2 cstrs
-    else compare_cumulative_instances cv_pb  variances u1 u2 cstrs
+    else
+      compare_cumulative_instances cv_pb variances ?sort_variance:mind.Declarations.mind_sort_variance u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
@@ -768,6 +769,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
+      let u1, u2 = UVars.normalize_sort_cumul_instances mind.Declarations.mind_sort_variance u1 u2 in
       let qs1, us1 = UVars.Instance.to_array u1
       and qs2, us2 = UVars.Instance.to_array u2 in
       let cstrs = enforce_eq_qualities qs1 qs2 cstrs in
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5baa9e7ac426..2a4809cca241 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -764,7 +764,8 @@ let subterm_source evk ?where (loc,k) =
 
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
-let compare_cumulative_instances cv_pb variances u u' sigma =
+let compare_cumulative_instances cv_pb variances ?sort_variance u u' sigma =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let open UnivProblem in
   let cstrs = Univ.UnivConstraints.empty in
   let soft = Set.empty in
@@ -788,7 +789,8 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
     Inl (Evd.add_constraints sigma soft)
   | exception UGraph.UniverseInconsistency p -> Inr p
 
-let compare_constructor_instances evd u u' =
+let compare_constructor_instances ?sort_variance evd u u' =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let open UnivProblem in
   let qs, us = UVars.Instance.to_array u
   and qs', us' = UVars.Instance.to_array u' in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index dcd6036b5b1c..42320569f946 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -180,6 +180,7 @@ val eq_constr_univs_test :
    Additionally flexible universes in irrelevant positions are unified
    if possible. Returns [Inr p] when the former is impossible. *)
 val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array ->
+  ?sort_variance:UVars.Variance.t array ->
   UVars.Instance.t -> UVars.Instance.t -> evar_map ->
   (evar_map, UGraph.univ_inconsistency) Util.union
 
@@ -188,7 +189,7 @@ val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array
 
     But what about qualities?
 *)
-val compare_constructor_instances : evar_map ->
+val compare_constructor_instances : ?sort_variance:UVars.Variance.t array -> evar_map ->
   UVars.Instance.t -> UVars.Instance.t -> (evar_map, UGraph.univ_inconsistency) Util.union
 
 (** {6 Unification problems} *)
diff --git a/engine/polyFlags.ml b/engine/polyFlags.ml
index f80fd4f3790e..7ab0b1fd711d 100644
--- a/engine/polyFlags.ml
+++ b/engine/polyFlags.ml
@@ -12,26 +12,31 @@ type t = {
   univ_poly : bool;
   collapse_sort_variables : bool;
   cumulative : bool;
+  sort_cumulative : bool;
 }
 
-let make ~univ_poly ~collapse_sort_variables ~cumulative =
+let make ~univ_poly ~collapse_sort_variables ~cumulative ~sort_cumulative =
   if cumulative && not univ_poly then
     CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions");
+  if sort_cumulative && not cumulative then
+    CErrors.user_err Pp.(str "Sort cumulativity requires universe cumulativity.");
   if not collapse_sort_variables && not univ_poly then
     CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions");
-  { collapse_sort_variables; univ_poly; cumulative }
+  { collapse_sort_variables; univ_poly; cumulative; sort_cumulative }
 
-let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false }
+let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false; sort_cumulative = false }
 let of_univ_poly b = { default with univ_poly = b }
 
 let collapse_sort_variables x = x.collapse_sort_variables
 let univ_poly x = x.univ_poly
 let cumulative x = x.cumulative
+let sort_cumulative x = x.sort_cumulative
 
 let pr f =
   let open Pp in
   str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++
   str "; cumulative = " ++ bool f.cumulative ++ spc () ++
+  str "; sort_cumulative = " ++ bool f.sort_cumulative ++ spc () ++
   str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++
   str "}"
 
diff --git a/engine/polyFlags.mli b/engine/polyFlags.mli
index 54ff95de64a3..c865092ba259 100644
--- a/engine/polyFlags.mli
+++ b/engine/polyFlags.mli
@@ -16,7 +16,7 @@ type t
  *)
 
 (** Raises a user error if [univ_poly = false] and either [collapse_sort_variables = false] or [cumulative = true]. *)
-val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> t
+val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> sort_cumulative:bool -> t
 
 (** The [default] is monomorphic:
     [univ_poly] and [cumulative] are [false], [collapse_sort_variables] is [true] *)
@@ -32,6 +32,7 @@ val of_univ_poly : bool -> t
 val univ_poly : t -> bool
 val collapse_sort_variables : t -> bool
 val cumulative : t -> bool
+val sort_cumulative : t -> bool
 
 (** Pretty print *)
 val pr : t -> Pp.t
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 4bfccc5ac207..54817c0a5562 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -127,7 +127,8 @@ let enforce_eq_qualities qs qs' cstrs =
       if Sorts.Quality.equal a b then c else Set.add (QEq (a, b)) c)
     cstrs qs qs'
 
-let compare_cumulative_instances  cv_pb variances u u' cstrs =
+let compare_cumulative_instances  cv_pb variances ?sort_variance u u' cstrs =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let make u = Sorts.sort_of_univ @@ Univ.Universe.make u in
   let qs, us = UVars.Instance.to_array u
   and qs', us' = UVars.Instance.to_array u' in
diff --git a/engine/univProblem.mli b/engine/univProblem.mli
index 6f53d88c83b4..b94706775171 100644
--- a/engine/univProblem.mli
+++ b/engine/univProblem.mli
@@ -49,4 +49,4 @@ val enforce_eq_instances_univs : bool -> Instance.t constraint_function
 
 val enforce_eq_qualities : Sorts.Quality.t array constraint_function
 
-val compare_cumulative_instances : Conversion.conv_pb -> Variance.t array -> Instance.t constraint_function
+val compare_cumulative_instances : Conversion.conv_pb -> Variance.t array -> ?sort_variance:Variance.t array -> Instance.t constraint_function
diff --git a/kernel/conversion.ml b/kernel/conversion.ml
index aa4c0bd3a1a4..f29d40669fc1 100644
--- a/kernel/conversion.ml
+++ b/kernel/conversion.ml
@@ -151,7 +151,7 @@ type conv_pb =
 type ('a, 'err) universe_compare = {
   compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
   compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
-  compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
+  compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
     UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
@@ -169,15 +169,15 @@ let convert_instances ~flex u u' (s, check) =
 
 exception MustExpand
 
-let convert_instances_cumul pb var u u' (s, check) =
-  (check.compare_cumul_instances pb var u u' s, check)
+let convert_instances_cumul pb var sort_var u u' (s, check) =
+  (check.compare_cumul_instances pb var sort_var u u' s, check)
 
-let get_cumulativity_constraints cv_pb variance u u' =
+let get_cumulativity_constraints cv_pb variance sort_variance u u' =
   match cv_pb with
   | CONV ->
-    UVars.enforce_eq_variance_instances variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
+    UVars.enforce_eq_variance_instances variance ?sort_variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
   | CUMUL ->
-    UVars.enforce_leq_variance_instances variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
+    UVars.enforce_leq_variance_instances variance ?sort_variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
 
 let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_nparams +
@@ -192,7 +192,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
       (* shortcut, not sure if worth doing, could use perf data *)
       if UVars.Instance.equal u1 u2 then Result.Ok s else raise MustExpand
     else
-      cmp_cumul cv_pb variances u1 u2 s
+      cmp_cumul cv_pb variances mind.Declarations.mind_sort_variance u1 u2 s
 
 type 'e conv_tab = {
   cnv_inf : clos_infos;
@@ -227,9 +227,8 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
     else
       (** By invariant, both constructors have a common supertype,
           so they are convertible _at that type_. *)
-      (* NB: no variance for qualities *)
       let variance = Array.make (snd (UVars.Instance.length u1)) UVars.Variance.Irrelevant in
-      cmp_cumul CONV variance u1 u2 s
+      cmp_cumul CONV variance mind.Declarations.mind_sort_variance u1 u2 s
 
 let convert_constructors ctor nargs u1 u2 (s, check) =
   convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -780,7 +779,7 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
     | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
       let len = Parray.length_int t1 in
       if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
-      let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
+      let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] None u1 u2 cuniv in
       let el1 = el_stack lft1 v1 in
       let el2 = el_stack lft2 v2 in
       let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -862,7 +861,7 @@ and convert_stacks ?(mask = [||]) l2r infos lft1 lft2 stk1 stk2 cuniv =
                     let u2 = CClosure.usubst_instance e2 u2 in
                     match mind.Declarations.mind_variance with
                     | None -> convert_instances ~flex:false u1 u2 cu
-                    | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
+                    | Some variances -> convert_instances_cumul CONV variances mind.Declarations.mind_sort_variance u1 u2 cu
                 in
                 let cu = fail_check infos cu in
                 let pms1 = mk_clos_vect e1 pms1 in
@@ -993,8 +992,8 @@ let check_convert_instances qeq = (); fun ~flex:_ u u' state ->
   else Result.Error None
 
 (* general conversion and inference functions *)
-let check_inductive_instances qeq = (); fun cv_pb variance u1 u2 state ->
-  let qcsts, ucsts = get_cumulativity_constraints cv_pb variance u1 u2 in
+let check_inductive_instances qeq = (); fun cv_pb variance sort_variance u1 u2 state ->
+  let qcsts, ucsts = get_cumulativity_constraints cv_pb variance sort_variance u1 u2 in
   let check_quality (q1, q2) = qeq q1 q2 in
   if UVars.QPairSet.for_all check_quality qcsts && UGraph.check_constraints ucsts state
   then Result.Ok state
diff --git a/kernel/conversion.mli b/kernel/conversion.mli
index d42217f8e0f5..14a1fe4cea65 100644
--- a/kernel/conversion.mli
+++ b/kernel/conversion.mli
@@ -25,7 +25,7 @@ type conv_pb = CONV | CUMUL
 type ('a, 'err) universe_compare = {
   compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
   compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
-  compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
+  compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
     UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
@@ -33,7 +33,7 @@ type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
 
 type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> constr -> constr -> ('a, 'err option) result
 
-val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array ->
+val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
   UVars.Instance.t -> UVars.Instance.t -> UVars.QPairSet.t * Univ.UnivConstraints.t
 
 val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 02b5b0e2a9fe..5cc676f75daa 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -298,6 +298,13 @@ type mutual_inductive_body = {
        outside sections. The final variance once all sections are
        discharged is [mind_sec_variance ++ mind_variance]. *)
 
+    mind_sort_variance : UVars.Variance.t array option;
+    (** Sort/quality variance info, [None] when no sort cumulativity. *)
+
+    mind_sec_sort_variance : UVars.Variance.t array option;
+    (** Sort variance info for section polymorphic qualities. [None]
+       outside sections. *)
+
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
     mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7dab6c0dca99..44bc39db67fa 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -270,6 +270,8 @@ let subst_mind_body subst mib =
     mind_template = mib.mind_template;
     mind_variance = mib.mind_variance;
     mind_sec_variance = mib.mind_sec_variance;
+    mind_sort_variance = mib.mind_sort_variance;
+    mind_sec_sort_variance = mib.mind_sec_sort_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
diff --git a/kernel/discharge.ml b/kernel/discharge.ml
index 466a76bb9681..0173209e882c 100644
--- a/kernel/discharge.ml
+++ b/kernel/discharge.ml
@@ -187,6 +187,17 @@ let cook_inductive info mib =
       in
       Some (Array.append newvariance variance), Some sec_variance
   in
+  let mind_sort_variance, mind_sec_sort_variance =
+    match mib.mind_sort_variance, mib.mind_sec_sort_variance with
+    | None, None -> None, None
+    | None, Some _ | Some _, None -> assert false
+    | Some variance, Some sec_variance ->
+      let qlen = fst (AbstractContext.size (universe_context_of_cooking_info info)) in
+      let sec_variance, newvariance =
+        Array.chop (Array.length sec_variance - qlen) sec_variance
+      in
+      Some (Array.append newvariance variance), Some sec_variance
+  in
   let mind_template = match mib.mind_template with
   | None -> None
   | Some {template_param_arguments=levels; template_context; template_concl; template_defaults;} ->
@@ -206,6 +217,8 @@ let cook_inductive info mib =
     mind_template;
     mind_variance;
     mind_sec_variance;
+    mind_sort_variance;
+    mind_sec_sort_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
diff --git a/kernel/entries.mli b/kernel/entries.mli
index f59c54d2d833..522e81049ce2 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -65,6 +65,10 @@ type mutual_inductive_entry = {
   (* [None] if non-cumulative, otherwise associates each universe of
      the entry to [None] if to be inferred or [Some v] if to be
      checked. *)
+  mind_entry_sort_variance : variance_entry option;
+  (* [None] if no sort cumulativity, otherwise associates each quality
+     of the entry to [None] if to be inferred or [Some v] if to be
+     checked. *)
   mind_entry_private : bool option;
 }
 
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 72c644c19b56..a709bb569c89 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -586,6 +586,8 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
         data, Some None, Some reason (* back to FakeRecord with a reason why *)
   in
 
+  let arities_for_variance = List.map (fun e -> e.mind_entry_arity) mie.mind_entry_inds in
+  let ctors_for_variance = List.map (fun e -> e.mind_entry_lc) mie.mind_entry_inds in
   let variance = match mie.mind_entry_variance with
     | None -> None
     | Some variances ->
@@ -605,12 +607,40 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
             Array.append sec_univs univs
         in
         let variances = InferCumulativity.infer_inductive ~env_params ~env_ar_par
-            ~arities:(List.map (fun e -> e.mind_entry_arity) mie.mind_entry_inds)
-            ~ctors:(List.map (fun e -> e.mind_entry_lc) mie.mind_entry_inds)
+            ~arities:arities_for_variance
+            ~ctors:ctors_for_variance
             univs
         in
         Some variances
   in
+  let sort_variance = match mie.mind_entry_sort_variance with
+    | None -> None
+    | Some sort_variances ->
+      match mie.mind_entry_universes with
+      | Monomorphic_ind_entry | Template_ind_entry _ ->
+        CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and sort cumulative.")
+      | Polymorphic_ind_entry uctx ->
+        let qualities, _univs = Instance.to_array @@ UContext.instance uctx in
+        let qvars = Array.map (fun q -> match q with
+          | Sorts.Quality.QVar qv -> qv
+          | _ -> assert false) qualities in
+        let qvars = Array.map2 (fun a b -> a,b) qvars sort_variances in
+        let qvars = match sec_univs with
+          | None -> qvars
+          | Some sec_univs ->
+            let sec_qs, _ = UVars.Instance.to_array sec_univs in
+            let sec_qvars = Array.map (fun q -> match q with
+              | Sorts.Quality.QVar qv -> qv, None
+              | _ -> assert false) sec_qs in
+            Array.append sec_qvars qvars
+        in
+        let sort_variances = InferCumulativity.infer_sort_variance ~env_params ~env_ar_par
+            ~arities:arities_for_variance
+            ~ctors:ctors_for_variance
+            qvars
+        in
+        Some sort_variances
+  in
 
   (* Abstract universes *)
   let usubst, univs = match mie.mind_entry_universes with
@@ -634,4 +664,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, template, variance, record, not_prim_reason_or_has_eta, params, Array.of_list data
+  env_ar_par, univs, template, variance, sort_variance, record, not_prim_reason_or_has_eta, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 1b2a149ab314..009cf6b2d604 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -45,6 +45,7 @@ val typecheck_inductive : env -> sec_univs:UVars.Instance.t option
   * universes
   * template_universes option
   * UVars.Variance.t array option
+  * UVars.Variance.t array option
   * Names.Id.t array option option
   * (Declarations.has_eta, NotPrimRecordReason.t) result option
   * Constr.rel_context
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index efafbf9c066a..b18136f8f589 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -494,7 +494,7 @@ let compute_projections ind ~nparamargs ~nf_lc ~consnrealdecls =
   Array.of_list (List.rev rs),
   Array.of_list (List.rev pbs)
 
-let build_inductive env ~sec_univs names prv univs template variance
+let build_inductive env ~sec_univs names prv univs template variance sort_variance
     paramsctxt kn isrecord isfinite inds nmr recargs not_prim_or_has_eta =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
@@ -579,6 +579,15 @@ let build_inductive env ~sec_univs names prv univs template variance
         Some (Array.sub variance nsecu (Array.length variance - nsecu)),
         Some (Array.sub variance 0 nsecu)
   in
+  let sort_variance, sec_sort_variance = match sort_variance with
+    | None -> None, None
+    | Some sort_variance -> match sec_univs with
+      | None -> Some sort_variance, None
+      | Some sec_univs ->
+        let nsecq, _nsecu = UVars.Instance.length sec_univs in
+        Some (Array.sub sort_variance nsecq (Array.length sort_variance - nsecq)),
+        Some (Array.sub sort_variance 0 nsecq)
+  in
   let univ_hyps = match sec_univs with
     | None -> UVars.Instance.empty
     | Some univs -> univs
@@ -595,6 +604,8 @@ let build_inductive env ~sec_univs names prv univs template variance
     mind_template = template;
     mind_variance = variance;
     mind_sec_variance = sec_variance;
+    mind_sort_variance = sort_variance;
+    mind_sec_sort_variance = sec_sort_variance;
     mind_private = prv;
     mind_typing_flags = Environ.typing_flags env;
   }
@@ -604,7 +615,7 @@ let build_inductive env ~sec_univs names prv univs template variance
 
 let check_inductive env ~sec_univs kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, template, variance, record, not_prim_reason_or_has_eta, paramsctxt, inds) =
+  let (env_ar_par, univs, template, variance, sort_variance, record, not_prim_reason_or_has_eta, paramsctxt, inds) =
     IndTyping.typecheck_inductive env ~sec_univs mie
   in
   (* Then check positivity conditions *)
@@ -618,7 +629,7 @@ let check_inductive env ~sec_univs kn mie =
   in
   (* Build the inductive packets *)
   let mib =
-    build_inductive env ~sec_univs names mie.mind_entry_private univs template variance
+    build_inductive env ~sec_univs names mie.mind_entry_private univs template variance sort_variance
       paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs not_prim_reason_or_has_eta
   in
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 9116b5713386..40f3eefa6bca 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -106,6 +106,67 @@ end = struct
 end
 open Inf
 
+(** Sort variance inference for quality variables *)
+module SortInf : sig
+  type sort_variances
+  val infer_quality_eq : Sorts.QVar.t -> sort_variances -> sort_variances
+  val infer_quality_leq : Sorts.QVar.t -> sort_variances -> sort_variances
+  val start : (Sorts.QVar.t * Variance.t option) array -> sort_variances
+  val finish : sort_variances -> Variance.t array
+end = struct
+  type inferred = IrrelevantI | CovariantI
+  type mode = Check | Infer
+
+  type sort_variances = {
+    orig_array : (Sorts.QVar.t * Variance.t option) array;
+    qvars : (mode * inferred) Sorts.QVar.Map.t;
+  }
+
+  let to_variance = function
+    | IrrelevantI -> Irrelevant
+    | CovariantI -> Covariant
+
+  let to_variance_opt o = Option.cata to_variance Invariant o
+
+  let infer_quality_eq q (sv : sort_variances) =
+    match Sorts.QVar.Map.find_opt q sv.qvars with
+    | None -> sv
+    | Some (Check, expected) ->
+      let expected = to_variance expected in
+      raise (BadVariance (Level.var 0, expected, Invariant)) (* reuse exception; the level is a dummy *)
+    | Some (Infer, _) ->
+      let qvars = Sorts.QVar.Map.remove q sv.qvars in
+      {sv with qvars}
+
+  let infer_quality_leq q sv =
+    let qvars =
+      Sorts.QVar.Map.update q (function
+        | None -> None
+        | Some (_, CovariantI) as x -> x
+        | Some (Infer, IrrelevantI) -> Some (Infer, CovariantI)
+        | Some (Check, IrrelevantI) ->
+          raise (BadVariance (Level.var 0, Irrelevant, Covariant)))
+        sv.qvars
+    in
+    if qvars == sv.qvars then sv else {sv with qvars}
+
+  let start qs =
+    let qvars = Array.fold_left (fun qvars (q, variance) ->
+        match variance with
+        | None -> Sorts.QVar.Map.add q (Infer, IrrelevantI) qvars
+        | Some Invariant -> qvars
+        | Some Covariant -> Sorts.QVar.Map.add q (Check, CovariantI) qvars
+        | Some Irrelevant -> Sorts.QVar.Map.add q (Check, IrrelevantI) qvars)
+        Sorts.QVar.Map.empty qs
+    in
+    {qvars; orig_array = qs}
+
+  let finish (sv : sort_variances) =
+    Array.map
+      (fun (q, _check) -> to_variance_opt (Option.map snd (Sorts.QVar.Map.find_opt q sv.qvars)))
+      sv.orig_array
+end
+
 let infer_generic_instance_eq variances u =
   Array.fold_left (fun variances u -> infer_level_eq u variances)
     variances
@@ -331,3 +392,96 @@ let infer_inductive ~env_params ~env_ar_par ~arities ~ctors univs =
   | TrivialVariance -> Array.make (Array.length univs) Invariant
   | BadVariance (lev, expected, actual) ->
     Type_errors.error_bad_variance env_params ~lev ~expected ~actual
+
+(** Infer sort (quality) variance by walking arities and constructors.
+    Quality variables that appear in CONV positions become Invariant,
+    those only in CUMUL positions become Covariant, otherwise Irrelevant.
+
+    We reuse the same infrastructure as universe variance inference:
+    walk terms with CClosure, and when we encounter a Sort, extract its
+    quality variable. *)
+
+let infer_sort_quality_of_sort cv_pb sv s =
+  let q = Sorts.quality s in
+  match q with
+  | Sorts.Quality.QVar qv ->
+    begin match cv_pb with
+    | CONV -> SortInf.infer_quality_eq qv sv
+    | CUMUL -> SortInf.infer_quality_leq qv sv
+    end
+  | Sorts.Quality.QConstant _ -> sv
+
+(** Collect all sorts occurring in a term and infer quality variance.
+    We walk the term structure similarly to infer_arity_constructor. *)
+let rec collect_sorts_in_constr cv_pb env sv c =
+  let open Constr in
+  match kind c with
+  | Sort s -> infer_sort_quality_of_sort cv_pb sv s
+  | Prod (_, a, b) ->
+    let sv = collect_sorts_in_constr CONV env sv a in
+    collect_sorts_in_constr cv_pb env sv b
+  | Lambda (_, a, b) ->
+    let sv = collect_sorts_in_constr CONV env sv a in
+    collect_sorts_in_constr CONV env sv b
+  | LetIn (_, b, t, c) ->
+    let sv = collect_sorts_in_constr CONV env sv b in
+    let sv = collect_sorts_in_constr CONV env sv t in
+    collect_sorts_in_constr cv_pb env sv c
+  | App (f, args) ->
+    let sv = collect_sorts_in_constr CONV env sv f in
+    Array.fold_left (fun sv arg -> collect_sorts_in_constr CONV env sv arg) sv args
+  | Ind (_, u) | Const (_, u) ->
+    let qs, _ = UVars.Instance.to_array u in
+    Array.fold_left (fun sv q ->
+      match q with
+      | Sorts.Quality.QVar qv -> SortInf.infer_quality_eq qv sv
+      | _ -> sv) sv qs
+  | Construct (_, u) ->
+    let qs, _ = UVars.Instance.to_array u in
+    Array.fold_left (fun sv q ->
+      match q with
+      | Sorts.Quality.QVar qv -> SortInf.infer_quality_eq qv sv
+      | _ -> sv) sv qs
+  | Case (_, u, _, _, _, _, _) ->
+    let qs, _ = UVars.Instance.to_array u in
+    Array.fold_left (fun sv q ->
+      match q with
+      | Sorts.Quality.QVar qv -> SortInf.infer_quality_eq qv sv
+      | _ -> sv) sv qs
+  | Fix (_, (_, tys, bds)) | CoFix (_, (_, tys, bds)) ->
+    let sv = Array.fold_left (fun sv t -> collect_sorts_in_constr CONV env sv t) sv tys in
+    Array.fold_left (fun sv b -> collect_sorts_in_constr CONV env sv b) sv bds
+  | Cast (c, _, t) ->
+    let sv = collect_sorts_in_constr cv_pb env sv c in
+    collect_sorts_in_constr CONV env sv t
+  | _ -> sv
+
+let infer_sort_arity_constructor is_arity env sv arcn =
+  let typs, codom = Reduction.whd_decompose_prod env arcn in
+  let sv = Context.Rel.fold_outside (fun typ sv ->
+    match typ with
+    | Context.Rel.Declaration.LocalAssum (_, t) -> collect_sorts_in_constr CONV env sv t
+    | Context.Rel.Declaration.LocalDef (_, b, t) ->
+      let sv = collect_sorts_in_constr CONV env sv b in
+      collect_sorts_in_constr CONV env sv t
+  ) typs ~init:sv in
+  if not is_arity then collect_sorts_in_constr CUMUL env sv codom
+  else sv
+
+let infer_sort_variance_core ~env_params ~env_ar_par ~arities ~ctors qvars =
+  let sv = SortInf.start qvars in
+  let sv = List.fold_left (fun sv arity ->
+      infer_sort_arity_constructor true env_params sv arity)
+      sv arities
+  in
+  let sv = List.fold_left
+      (List.fold_left (infer_sort_arity_constructor false env_ar_par))
+      sv ctors
+  in
+  SortInf.finish sv
+
+let infer_sort_variance ~env_params ~env_ar_par ~arities ~ctors qvars =
+  try infer_sort_variance_core ~env_params ~env_ar_par ~arities ~ctors qvars
+  with BadVariance (_lev, _expected, _actual) ->
+    (* If sort variance checking fails, default to all Invariant *)
+    Array.make (Array.length qvars) Invariant
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index 7b405d11eea6..e1870c2ca53e 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -19,3 +19,12 @@ val infer_inductive
   -> (Univ.Level.t * UVars.Variance.t option) array
   (** Universes whose cumulativity we want to infer or check. *)
   -> UVars.Variance.t array
+
+val infer_sort_variance
+  : env_params : Environ.env
+  -> env_ar_par : Environ.env
+  -> arities : Constr.t list
+  -> ctors : Constr.t list list
+  -> (Sorts.QVar.t * UVars.Variance.t option) array
+  (** Quality variables whose sort cumulativity we want to infer or check. *)
+  -> UVars.Variance.t array
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 67b14efe4fb7..9229f8274d0b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -148,6 +148,7 @@ let check_inductive (cst, ustate) trace env mp1 l info1 mp2 mib2 subst1 subst2 r
   in
   let env = check_universes error env mib1.mind_universes mib2.mind_universes in
   let () = check_variance error mib1.mind_variance mib2.mind_variance in
+  let () = check_variance error mib1.mind_sort_variance mib2.mind_sort_variance in
   let inst = make_abstract_instance (Declareops.inductive_polymorphic_context mib1) in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name t1 t2 =
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2f837f7afbb9..a89628ea8b00 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -539,7 +539,8 @@ let type_case_scrutinee env (mib, _mip) (u', largs) u pms (pctx, p) c =
      flipped. It is relevant for performance eg in bedrock / Kami. *)
   let qcst, ucst = match mib.mind_variance with
   | None -> UVars.enforce_eq_instances u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
-  | Some variance -> UVars.enforce_leq_variance_instances variance u' u (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
+  | Some variance ->
+    UVars.enforce_leq_variance_instances variance ?sort_variance:mib.mind_sort_variance u' u (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
   in
   let () = check_pconstraints (qcst, ucst) env in
   let subst = Vars.subst_of_rel_context_instance_list pctx (realargs @ [c]) in
diff --git a/kernel/uVars.ml b/kernel/uVars.ml
index adba4cf906c2..21c06d887211 100644
--- a/kernel/uVars.ml
+++ b/kernel/uVars.ml
@@ -212,13 +212,47 @@ let enforce_eq_instances x y (qcs, ucs as orig) =
   let ucs' = CArray.fold_right2 enforce_eq_level xu yu ucs in
   if qcs' == qcs && ucs' == ucs then orig else qcs', ucs'
 
-let enforce_eq_variance_instances variances x y (qcs,ucs as orig) =
+let quality_same_component q1 q2 =
+  let open Quality in
+  match q1, q2 with
+  | QConstant Sorts.Quality.QProp, QConstant Sorts.Quality.QProp -> true
+  | QConstant Sorts.Quality.QProp, QConstant Sorts.Quality.QType -> true
+  | QConstant Sorts.Quality.QType, QConstant Sorts.Quality.QProp -> true
+  | QConstant Sorts.Quality.QType, QConstant Sorts.Quality.QType -> true
+  | QConstant Sorts.Quality.QSProp, QConstant Sorts.Quality.QSProp -> true
+  | QVar v1, QVar v2 -> Sorts.QVar.equal v1 v2
+  | _ -> false
+
+let normalize_sort_cumul_instances sort_variances u1 u2 =
+  match sort_variances with
+  | None -> u1, u2
+  | Some sv ->
+    let q1, l1 = Instance.to_array u1 and q2, l2 = Instance.to_array u2 in
+    let q1 = Array.copy q1 and q2 = Array.copy q2 in
+    let changed = ref false in
+    Array.iteri (fun i v ->
+      match v with
+      | Variance.Irrelevant | Variance.Covariant ->
+        if quality_same_component q1.(i) q2.(i) && not (Quality.equal q1.(i) q2.(i)) then begin
+          q1.(i) <- Quality.qtype;
+          q2.(i) <- Quality.qtype;
+          changed := true
+        end
+      | Variance.Invariant -> ()) sv;
+    if !changed then
+      Instance.of_array (q1, l1), Instance.of_array (q2, l2)
+    else
+      u1, u2
+
+let enforce_eq_variance_instances variances ?sort_variance x y (qcs,ucs as orig) =
+  let x, y = normalize_sort_cumul_instances sort_variance x y in
   let xq, xu = Instance.to_array x and yq, yu = Instance.to_array y in
   let qcs' = CArray.fold_right2 enforce_eq_cumul_quality xq yq qcs in
   let ucs' = Variance.eq_constraints variances xu yu ucs in
   if qcs' == qcs && ucs' == ucs then orig else qcs', ucs'
 
-let enforce_leq_variance_instances variances x y (qcs,ucs as orig) =
+let enforce_leq_variance_instances variances ?sort_variance x y (qcs,ucs as orig) =
+  let x, y = normalize_sort_cumul_instances sort_variance x y in
   let xq, xu = Instance.to_array x and yq, yu = Instance.to_array y in
   (* no variance for quality variables -> enforce_eq *)
   let qcs' = CArray.fold_right2 enforce_eq_cumul_quality xq yq qcs in
diff --git a/kernel/uVars.mli b/kernel/uVars.mli
index e327591d4142..f25482ff457a 100644
--- a/kernel/uVars.mli
+++ b/kernel/uVars.mli
@@ -91,8 +91,19 @@ type 'a pconstraints_function = 'a -> 'a -> QPairSet.t * UnivConstraints.t -> QP
 
 val enforce_eq_instances : Instance.t pconstraints_function
 
-val enforce_eq_variance_instances : Variance.t array -> Instance.t pconstraints_function
-val enforce_leq_variance_instances : Variance.t array -> Instance.t pconstraints_function
+val enforce_eq_variance_instances : Variance.t array -> ?sort_variance:Variance.t array -> Instance.t pconstraints_function
+val enforce_leq_variance_instances : Variance.t array -> ?sort_variance:Variance.t array -> Instance.t pconstraints_function
+
+val quality_same_component : Sorts.Quality.t -> Sorts.Quality.t -> bool
+(** Returns [true] if both qualities are in the same connected component:
+    {Prop, Type/Set} or {SProp}. *)
+
+val normalize_sort_cumul_instances : Variance.t array option -> Instance.t -> Instance.t -> Instance.t * Instance.t
+(** [normalize_sort_cumul_instances sort_variances u1 u2] normalizes
+    quality positions with non-Invariant sort variance where both qualities
+    are in the same connected component, replacing both with a canonical
+    representative (QType). This makes the existing quality equality checks
+    pass transparently for sort-cumulative positions. *)
 
 type 'a puniverses = 'a * Instance.t
 val out_punivs : 'a puniverses -> 'a
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6535830e2bbe..37e85997aa53 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -465,14 +465,14 @@ let rec ise_app_rev_stack2 env f evd revsk1 revsk2 =
 
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
-let compare_cumulative_instances pbty evd variances u u' =
-  match Evarutil.compare_cumulative_instances pbty variances u u' evd with
+let compare_cumulative_instances pbty evd variances ?sort_variance u u' =
+  match Evarutil.compare_cumulative_instances pbty variances ?sort_variance u u' evd with
   | Inl evd ->
     Success evd
   | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
 
-let compare_constructor_instances evd u u' =
-  match Evarutil.compare_constructor_instances evd u u' with
+let compare_constructor_instances ?sort_variance evd u u' =
+  match Evarutil.compare_constructor_instances ?sort_variance evd u u' with
   | Inl evd ->
     Success evd
   | Inr p -> UnifFailure (evd, UnifUnivInconsistency p)
@@ -515,7 +515,7 @@ let compare_heads pbty env evd ~nargs term term' =
           if not (is_applied nargs needed)
           then check_strict evd u u'
           else
-            compare_cumulative_instances pbty evd variances u u'
+            compare_cumulative_instances pbty evd variances ?sort_variance:mind.mind_sort_variance u u'
       end
   | Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
   | Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
@@ -531,7 +531,8 @@ let compare_heads pbty env evd ~nargs term term' =
           let needed = Conversion.constructor_cumulativity_arguments (mind,ind,ctor) in
           if not (is_applied nargs needed)
           then check_strict evd u u'
-          else compare_constructor_instances evd u u'
+          else
+            compare_constructor_instances ?sort_variance:mind.mind_sort_variance evd u u'
       end
   | Construct _, Construct _ -> UnifFailure (evd, NotSameHead)
   | _, _ -> assert false
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1730bb25e60e..d63471296c7f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1229,8 +1229,8 @@ let check_convert_instances ~flex:_ u u' univs =
   if check_cumul_contraints univs cst then Result.Ok univs else Result.Error None
 
 (* general conversion and inference functions *)
-let check_inductive_instances cv_pb variance u1 u2 univs =
-  let cst = get_cumulativity_constraints cv_pb variance u1 u2 in
+let check_inductive_instances cv_pb variance sort_variance u1 u2 univs =
+  let cst = get_cumulativity_constraints cv_pb variance sort_variance u1 u2 in
   if check_cumul_contraints univs cst then Result.Ok univs else Result.Error None
 
 let checked_universes =
@@ -1279,7 +1279,7 @@ let is_conv_nounivs ?(reds=TransparentState.full) env sigma t1 t2 =
       let ignore_univs = let open Conversion in {
         compare_sorts = (fun _ _ _ () -> Ok ());
         compare_instances = (fun ~flex:_ _ _ () -> Ok ());
-        compare_cumul_instances = (fun _ _ _ _ () -> Ok ());
+        compare_cumul_instances = (fun _ _ _ _ _ () -> Ok ());
       }
       in
       begin match Conversion.generic_conv ~l2r:false CONV ~evars reds env ((), ignore_univs) t1 t2 with
@@ -1311,8 +1311,8 @@ let sigma_compare_instances ~flex i0 i1 sigma =
   | exception Evd.UniversesDiffer -> Result.Error None
   | exception UGraph.UniverseInconsistency err -> Result.Error (Some err)
 
-let sigma_check_inductive_instances cv_pb variance u1 u2 sigma =
-  match Evarutil.compare_cumulative_instances cv_pb variance u1 u2 sigma with
+let sigma_check_inductive_instances cv_pb variance sort_variance u1 u2 sigma =
+  match Evarutil.compare_cumulative_instances cv_pb variance ?sort_variance u1 u2 sigma with
   | Inl sigma -> Result.Ok sigma
   | Inr err -> Result.Error (Some err)
 
@@ -1331,8 +1331,8 @@ let univproblem_compare_sorts pb s0 s1 uset =
 let univproblem_compare_instances ~flex i0 i1 uset =
   Result.Ok (UnivProblem.enforce_eq_instances_univs flex i0 i1 uset)
 
-let univproblem_check_inductive_instances cv_pb variance u1 u2 sigma =
-  Result.Ok (UnivProblem.compare_cumulative_instances cv_pb variance u1 u2 sigma)
+let univproblem_check_inductive_instances cv_pb variance sort_variance u1 u2 sigma =
+  Result.Ok (UnivProblem.compare_cumulative_instances cv_pb variance ?sort_variance u1 u2 sigma)
 
 let univproblem_univ_state =
   let open Conversion in
@@ -1760,8 +1760,8 @@ let infer_convert_instances ~flex u u' (univs, cstrs as cuniv) =
   with UGraph.UniverseInconsistency err -> Result.Error (Some (Univ err))
 
 
-let infer_inductive_instances cv_pb variance u1 u2 (univs,csts) =
-  let qcsts, csts' = get_cumulativity_constraints cv_pb variance u1 u2 in
+let infer_inductive_instances cv_pb variance sort_variance u1 u2 (univs,csts) =
+  let qcsts, csts' = get_cumulativity_constraints cv_pb variance sort_variance u1 u2 in
   if check_eq_qualities qcsts then
     match UGraph.merge_constraints csts' univs with
     | univs -> Result.Ok (univs, Univ.UnivConstraints.union csts csts')
diff --git a/tactics/allScheme.ml b/tactics/allScheme.ml
index e3522d27f309..b9bdce33f7e1 100644
--- a/tactics/allScheme.ml
+++ b/tactics/allScheme.ml
@@ -950,6 +950,7 @@ let generate_all_aux suffix kn u sub_temp mib uparams strpos nuparams =
       mind_entry_inds = Array.to_list ind_bodies;
       mind_entry_universes = Polymorphic_ind_entry uctx;
       mind_entry_variance = Some (Array.make ulen None);
+      mind_entry_sort_variance = None;
       mind_entry_private = mib.mind_private;
       }
   in
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 4a9120f745c3..581f5c62c9d6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -216,7 +216,7 @@ let rec define_individual_scheme_base ?loc kind suff f ~internal idopt (mind,i a
     | None -> add_suffix mib.mind_packets.(i).mind_typename ("_"^suff) in
   let role = Evd.Schema (ind, kind) in
   let poly, cumulative = Declareops.inductive_is_polymorphic mib, Declareops.inductive_is_cumulative mib in
-  let poly = PolyFlags.make ~univ_poly:poly ~cumulative ~collapse_sort_variables:true in
+  let poly = PolyFlags.make ~univ_poly:poly ~cumulative ~sort_cumulative:false ~collapse_sort_variables:true in
   let const, eff = define ?loc internal role id c poly ctx eff in
   const, eff
 
diff --git a/test-suite/success/sort_cumulativity.v b/test-suite/success/sort_cumulativity.v
new file mode 100644
index 000000000000..2e68093aa67a
--- /dev/null
+++ b/test-suite/success/sort_cumulativity.v
@@ -0,0 +1,32 @@
+(* Test sort cumulativity for polymorphic inductive types *)
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Polymorphic Inductive Sort Cumulativity.
+
+(* A sort-polymorphic isomorphism record *)
+Record Iso@{s s'; u u'} (A : Type@{s; u}) (B : Type@{s'; u'}) : Type@{s; u} := {
+  iso_fun : A -> B ;
+  iso_inv : B -> A
+}.
+
+(* Test 1: Prop and Type are in the same connected component *)
+(* Prop -> Type in first sort position should succeed *)
+Axiom prop_iso : Iso@{Prop Prop; Set Set} True True.
+Check (prop_iso : Iso@{Type Prop; Set Set} True True).
+
+(* Test 2: Type -> Prop should also work (connected component, not ordering) *)
+Axiom type_iso : Iso@{Type Prop; Set Set} True True.
+Check (type_iso : Iso@{Prop Prop; Set Set} True True).
+
+(* Test 3: SProp is alone in its own connected component - SProp <-> Prop should fail *)
+Fail Check (prop_iso : Iso@{SProp Prop; Set Set} True True).
+
+(* Test 4: Without sort cumulativity, Prop -> Type should fail *)
+Unset Polymorphic Inductive Sort Cumulativity.
+Record Iso2@{s s'; u u'} (A : Type@{s; u}) (B : Type@{s'; u'}) : Type@{s; u} := {
+  iso2_fun : A -> B ;
+  iso2_inv : B -> A
+}.
+Axiom prop_iso2 : Iso2@{Prop Prop; Set Set} True True.
+Fail Check (prop_iso2 : Iso2@{Type Prop; Set Set} True True).
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 4e86dec2760e..c4a7b67bfc6f 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -297,6 +297,9 @@ let polymorphic =
 let { Goptions.get = is_polymorphic_inductive_cumulativity } =
   Goptions.declare_bool_option_and_ref ~key:["Polymorphic"; "Inductive"; "Cumulativity"] ~value:false ()
 
+let { Goptions.get = is_polymorphic_inductive_sort_cumulativity } =
+  Goptions.declare_bool_option_and_ref ~key:["Polymorphic"; "Inductive"; "Sort"; "Cumulativity"] ~value:false ()
+
 let { Goptions.get = should_collapse_sort_variables  } =
   Goptions.declare_bool_option_and_ref ~key:["Collapse"; "Sorts"; "ToType"] ~value:true ()
 
@@ -329,7 +332,8 @@ let poly kind =
         CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions.")
       else b
   in
-  return (PolyFlags.make ~univ_poly ~cumulative ~collapse_sort_variables)
+  let sort_cumulative = if cumulative then is_polymorphic_inductive_sort_cumulativity () else false in
+  return (PolyFlags.make ~univ_poly ~cumulative ~sort_cumulative ~collapse_sort_variables)
 
 let poly_def = poly PolyFlags.Definition
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8cfdc18778b8..a9f0e7f750b2 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -625,6 +625,16 @@ let variance_of_entry ~cumulative ~variances uctx =
       assert (lvs <= lus);
       Some (Array.append variances (Array.make (lus - lvs) None))
 
+let sort_variance_of_entry ~sort_cumulative uctx =
+  match uctx with
+  | Monomorphic_ind_entry | Template_ind_entry _ -> None
+  | Polymorphic_ind_entry uctx ->
+    if not sort_cumulative then None
+    else
+      let lqs, _ = UVars.UContext.size uctx in
+      if lqs = 0 then None
+      else Some (Array.make lqs None)
+
 let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~indnames ~arities_explicit ~arities ~template_syntax ~constructors ~env_ar ~private_ind =
   let {
     poly;
@@ -671,6 +681,7 @@ let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~
       indnames arities constructors
   in
   let variance = variance_of_entry ~cumulative:(PolyFlags.cumulative poly) ~variances univ_entry in
+  let sort_variance = sort_variance_of_entry ~sort_cumulative:(PolyFlags.sort_cumulative poly) univ_entry in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -680,6 +691,7 @@ let interp_mutual_inductive_constr ~sigma ~flags ~udecl ~variances ~ctx_params ~
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = univ_entry;
       mind_entry_variance = variance;
+      mind_entry_sort_variance = sort_variance;
     }
   in
   default_dep_elim, mind_ent, ubinders, global_univs
diff --git a/vernac/comRewriteRule.ml b/vernac/comRewriteRule.ml
index 2c7475891177..bf6f65322b2c 100644
--- a/vernac/comRewriteRule.ml
+++ b/vernac/comRewriteRule.ml
@@ -427,7 +427,7 @@ let interp_rule ~collapse_sort_variables (udecl, lhs, rhs: Constrexpr.universe_d
   let rhs_loc = rhs.CAst.loc in
 
   let lhs = Constrintern.(intern_gen WithoutTypeConstraint env evd lhs) in
-  let poly = PolyFlags.make ~univ_poly:true ~cumulative:false ~collapse_sort_variables in
+  let poly = PolyFlags.make ~univ_poly:true ~cumulative:false ~sort_cumulative:false ~collapse_sort_variables in
   let flags = { Pretyping.no_classes_no_fail_inference_flags with
     undeclared_evars_rr = true; expand_evars = false;
     solve_unification_constraints = false; poly } in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 5805bce664e1..92a9dea443e5 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -550,7 +550,7 @@ let do_scheme_all_predicate ?all_depth ~declare_mind kn mib strpos sAll keyAll =
   let sigma, (_, u) = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma (kn,0) in
   let (uctx, mentry) = AllScheme.generate_all_predicate env sigma kn u mib strpos sAll in
   (* declare it *)
-  let poly_flag = PolyFlags.make ~univ_poly:true ~collapse_sort_variables:true ~cumulative:true in
+  let poly_flag = PolyFlags.make ~univ_poly:true ~collapse_sort_variables:true ~cumulative:true ~sort_cumulative:false in
   let univs = UState.univ_entry ~poly:poly_flag uctx in
   let kn_nested = declare_mind ?all_depth mentry univs in
   (* register it *)
@@ -575,7 +575,7 @@ let do_scheme_all_theorem kn mib kn_nested focus strpos sAllThm keyAllThm =
   let uctx = UState.restrict uctx (Vars.universes_of_constr thm) in
   let sigma = Evd.set_universe_context sigma uctx in
   (* declare it *)
-  let poly_flag = PolyFlags.make ~univ_poly:true ~collapse_sort_variables:true ~cumulative:true in
+  let poly_flag = PolyFlags.make ~univ_poly:true ~collapse_sort_variables:true ~cumulative:true ~sort_cumulative:false in
   let info = Declare.Info.make ~poly:poly_flag () in
   let fth_name = Nameops.add_suffix mib.mind_packets.(focus).mind_typename sAllThm in
   let cinfo = Declare.CInfo.make ~name:fth_name ~typ:(None : (Evd.econstr option)) () in