diff --git a/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md b/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
index 32956cdfa8..4f054dd1ac 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
@@ -416,19 +416,44 @@ def mutually_bound[T: Base, U]():
 
 ## Nested typevars
 
-A typevar's constraint can _mention_ another typevar without _constraining_ it. In this example, `U`
-must be specialized to `list[T]`, but it cannot affect what `T` is specialized to.
+The specialization of one typevar can affect the specialization of another, even if it is not a
+"top-level" type in the bounds. (That is, if it appears as inside the specialization of a generic
+class.)
 
 ```py
 from typing import Never
 from ty_extensions import ConstraintSet, generic_context
 
-def mentions[T, U]():
-    # (T@mentions ≤ int) ∧ (U@mentions = list[T@mentions])
-    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T])
-    # TODO: revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
-    # revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = Unknown]
-    reveal_type(generic_context(mentions).specialize_constrained(constraints))
+class Covariant[T]:
+    def get(self) -> T:
+        raise NotImplementedError
+
+class Contravariant[T]:
+    def receive(self, input: T): ...
+
+class Invariant[T]:
+    mutable_attribute: T
+
+def mentions_covariant[T, U]():
+    # (T@mentions_covariant ≤ int) ∧ (U@mentions_covariant ≤ Covariant[T@mentions_covariant])
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T])
+    # TODO: revealed: ty_extensions.Specialization[T@mentions_covariant = int, U@mentions_covariant = Covariant[int]]
+    # revealed: ty_extensions.Specialization[T@mentions_covariant = int, U@mentions_covariant = Unknown]
+    reveal_type(generic_context(mentions_covariant).specialize_constrained(constraints))
+
+def mentions_contravariant[T, U]():
+    # (T@mentions_contravariant ≤ int) ∧ (Contravariant[T@mentions_contravariant] ≤ U@mentions_contravariant)
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object)
+    # TODO: revealed: ty_extensions.Specialization[T@mentions_contravariant = int, U@mentions_contravariant = Contravariant[int]]
+    # revealed: ty_extensions.Specialization[T@mentions_contravariant = int, U@mentions_contravariant = Unknown]
+    reveal_type(generic_context(mentions_contravariant).specialize_constrained(constraints))
+
+def mentions_invariant[T, U]():
+    # (T@mentions_invariant ≤ int) ∧ (U@mentions_invariant = Invariant[T@mentions_invariant])
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Invariant[T], U, Invariant[T])
+    # TODO: revealed: ty_extensions.Specialization[T@mentions_invariant = int, U@mentions_invariant = Invariant[int]]
+    # revealed: ty_extensions.Specialization[T@mentions_invariant = int, U@mentions_invariant = Unknown]
+    reveal_type(generic_context(mentions_invariant).specialize_constrained(constraints))
 ```
 
 If the constraint set contains mutually recursive bounds, specialization inference will not
@@ -437,8 +462,8 @@ this case.
 
 ```py
 def divergent[T, U]():
-    # (T@divergent = list[U@divergent]) ∧ (U@divergent = list[T@divergent]))
-    constraints = ConstraintSet.range(list[U], T, list[U]) & ConstraintSet.range(list[T], U, list[T])
+    # (T@divergent = Invariant[U@divergent]) ∧ (U@divergent = Invariant[T@divergent]))
+    constraints = ConstraintSet.range(Invariant[U], T, Invariant[U]) & ConstraintSet.range(Invariant[T], U, Invariant[T])
     # revealed: None
     reveal_type(generic_context(divergent).specialize_constrained(constraints))
 ```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/quantification.md b/crates/ty_python_semantic/resources/mdtest/type_properties/quantification.md
new file mode 100644
index 0000000000..a09c656351
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/quantification.md
@@ -0,0 +1,279 @@
+# Constraint set quantification
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+We can _existentially quantify_ a constraint set over a type variable. The result is a copy of the
+constraint set that only mentions the requested typevar. All constraints mentioning any other
+typevars are removed. Importantly, they are removed "safely", with their constraints propagated
+through to the remaining constraints as needed.
+
+## Keeping a single typevar
+
+If a constraint set only mentions a single typevar, and we keep that typevar when quantifying, the
+result is unchanged.
+
+```py
+from ty_extensions import ConstraintSet, static_assert
+
+class Base: ...
+class Sub(Base): ...
+
+def keep_single[T]():
+    constraints = ConstraintSet.always()
+    quantified = ConstraintSet.always()
+    static_assert(constraints.retain_one(T) == quantified)
+
+    constraints = ConstraintSet.never()
+    quantified = ConstraintSet.never()
+    static_assert(constraints.retain_one(T) == quantified)
+
+    constraints = ConstraintSet.range(Sub, T, Base)
+    quantified = ConstraintSet.range(Sub, T, Base)
+    static_assert(constraints.retain_one(T) == quantified)
+```
+
+## Removing a single typevar
+
+If a constraint set only mentions a single typevar, and we remove that typevar when quantifying,
+the result is usually "always". The only exception is if the original constraint set has no
+solution. In that case, the result is also unsatisfiable.
+
+```py
+from ty_extensions import ConstraintSet, static_assert
+
+class Base: ...
+class Sub(Base): ...
+
+def remove_single[T]():
+    constraints = ConstraintSet.always()
+    quantified = ConstraintSet.always()
+    static_assert(constraints.exists(T) == quantified)
+
+    constraints = ConstraintSet.never()
+    quantified = ConstraintSet.never()
+    static_assert(constraints.exists(T) == quantified)
+
+    constraints = ConstraintSet.range(Sub, T, Base)
+    quantified = ConstraintSet.always()
+    static_assert(constraints.exists(T) == quantified)
+```
+
+This also holds when the constraint set contains multiple typevars. In the cases below, we are
+keeping `U`, and the constraints on `T` do not ever affect what `U` can specialize to — `U` can
+specialize to anything (unless the original constraint set is unsatisfiable).
+
+```py
+from ty_extensions import ConstraintSet, static_assert
+
+class Base: ...
+class Sub(Base): ...
+
+def remove_other[T, U]():
+    constraints = ConstraintSet.always()
+    quantified = ConstraintSet.always()
+    static_assert(constraints.retain_one(U) == quantified)
+
+    constraints = ConstraintSet.never()
+    quantified = ConstraintSet.never()
+    static_assert(constraints.retain_one(U) == quantified)
+
+    constraints = ConstraintSet.range(Sub, T, Base)
+    quantified = ConstraintSet.always()
+    static_assert(constraints.retain_one(U) == quantified)
+```
+
+## Transitivity
+
+When a constraint set mentions two typevars, and compares them directly, then we can use
+transitivity to propagate the other constraints when quantifying.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+def transitivity[T, U]():
+    # (Base ≤ T) ∧ (T ≤ U) → (Base ≤ U)
+    constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(T, U, object)
+    quantified = ConstraintSet.range(Base, U, object)
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Base ≤ T ≤ Super) ∧ (T ≤ U) → (Base ≤ U)
+    constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(T, U, object)
+    quantified = ConstraintSet.range(Base, U, object)
+    static_assert(constraints.exists(T) == quantified)
+
+    # (T ≤ Base) ∧ (U ≤ T) → (U ≤ Base)
+    constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, T)
+    quantified = ConstraintSet.range(Never, U, Base)
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Sub ≤ T ≤ Base) ∧ (U ≤ T) → (U ≤ Base)
+    constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, T)
+    quantified = ConstraintSet.range(Never, U, Base)
+    static_assert(constraints.exists(T) == quantified)
+```
+
+## Covariant transitivity
+
+The same applies when one of the typevars is used covariantly in a bound of the other typevar.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise NotImplementedError
+
+def covariant_transitivity[T, U]():
+    # (Base ≤ T) ∧ (Covariant[T] ≤ U) → (Covariant[Base] ≤ U)
+    constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Covariant[T], U, object)
+    quantified = ConstraintSet.range(Covariant[Base], U, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Base ≤ T ≤ Super) ∧ (Covariant[T] ≤ U) → (Covariant[Base] ≤ U)
+    constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(Covariant[T], U, object)
+    quantified = ConstraintSet.range(Covariant[Base], U, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (T ≤ Base) ∧ (U ≤ Covariant[T]) → (U ≤ Covariant[Base])
+    constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, U, Covariant[T])
+    quantified = ConstraintSet.range(Never, U, Covariant[Base])
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Sub ≤ T ≤ Base) ∧ (U ≤ Covariant[T]) → (U ≤ Covariant[Base])
+    constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, Covariant[T])
+    quantified = ConstraintSet.range(Never, U, Covariant[Base])
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+```
+
+## Contravariant transitivity
+
+Similar rules apply, but in reverse, when one of the typevars is used contravariantly in a bound of
+the other typevar.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+class Contravariant[T]:
+    def receive(self, input: T): ...
+
+def contravariant_transitivity[T, U]():
+    # (Base ≤ T) ∧ (U ≤ Contravariant[T]) → (U ≤ Contravariant[Base])
+    constraints = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Never, U, Contravariant[T])
+    quantified = ConstraintSet.range(Never, U, Contravariant[Base])
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Base ≤ T ≤ Super) ∧ (U ≤ Contravariant[T]) → (U ≤ Contravariant[Base])
+    constraints = ConstraintSet.range(Base, T, Super) & ConstraintSet.range(Never, U, Contravariant[T])
+    quantified = ConstraintSet.range(Never, U, Contravariant[Base])
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (T ≤ Base) ∧ (Contravariant[T] ≤ U) → (Contravariant[Base] ≤ U)
+    constraints = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Contravariant[T], U, object)
+    quantified = ConstraintSet.range(Contravariant[Base], U, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Sub ≤ T ≤ Base) ∧ (Contravariant[T] ≤ U) → (Contravariant[Base] ≤ U)
+    constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Contravariant[T], U, object)
+    quantified = ConstraintSet.range(Contravariant[Base], U, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+```
+
+## Invariant transitivity involving equality constraints
+
+Invariant uses of a typevar are more subtle. The simplest case is when there is an _equality_
+constraint on the invariant typevar. In that case, we know precisely which specialization is
+required.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Base: ...
+
+class Invariant[T]:
+    mutable_attribute: T
+
+def invariant_equality_transitivity[T, U]():
+    # (T = Base) ∧ (U ≤ Invariant[T]) → (U ≤ Invariant[Base])
+    constraints = ConstraintSet.range(Base, T, Base) & ConstraintSet.range(Never, U, Invariant[T])
+    quantified = ConstraintSet.range(Never, U, Invariant[Base])
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (T = Base) ∧ (Invariant[T] ≤ U) → (Invariant[Base] ≤ U)
+    constraints = ConstraintSet.range(Base, T, Base) & ConstraintSet.range(Invariant[T], U, object)
+    quantified = ConstraintSet.range(Invariant[Base], U, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+```
+
+## Invariant transitivity involving range constraints
+
+When there is a _range_ constraint on the invariant typevar, we still have to retain information
+about which range of types the quantified-away typevar can specialize to, since this affects which
+types the remaining typevar can specialize to, and invariant typevars are not monotonic like
+covariant and contravariant typevars.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Base: ...
+class Sub(Base): ...
+
+class Invariant[T]:
+    mutable_attribute: T
+
+def invariant_range_transitivity[T, U]():
+    # (Sub ≤ T ≤ Base) ∧ (U ≤ Invariant[T]) → (U ≤ Invariant[Exists[Sub, Base]])
+    constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Never, U, Invariant[T])
+    # TODO: The existential that we need doesn't exist yet.
+    quantified = ConstraintSet.never()
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+
+    # (Sub ≤ T ≤ Base) ∧ (Invariant[T] ≤ U) → (Invariant[Exists[Sub, Base]] ≤ U)
+    constraints = ConstraintSet.range(Sub, T, Base) & ConstraintSet.range(Invariant[T], U, object)
+    # TODO: The existential that we need doesn't exist yet.
+    quantified = ConstraintSet.never()
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.exists(T) == quantified)
+```