diff --git a/docs/spec/annotations.rst b/docs/spec/annotations.rst
index 0b0ce641..4ebfd01b 100644
--- a/docs/spec/annotations.rst
+++ b/docs/spec/annotations.rst
@@ -16,13 +16,17 @@ hinting is used by filling function annotation slots with classes::
 This states that the expected type of the ``name`` argument is
 ``str``.  Analogically, the expected return type is ``str``.
 
-Expressions whose type is a subtype of a specific argument type are
-also accepted for that argument.
+Expressions whose type is :term:`assignable` to a specific argument type are
+also accepted for that argument. Similarly, an expression whose type is
+assignable to the annotated return type can be returned from the function.
 
 .. _`missing-annotations`:
 
-Any function without annotations should be treated as having the most
-general type possible, or ignored, by any type checker.
+Any function without annotations should be treated as having :ref:`Any`
+annotations on all arguments and the return type.
+
+Type checkers may choose to entirely ignore (not type check) the bodies of
+functions with no annotations, but this behavior is not required.
 
 It is recommended but not required that checked functions have
 annotations for all arguments and the return type.  For a checked
diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst
index 3ec63bfa..bc9c5396 100644
--- a/docs/spec/callables.rst
+++ b/docs/spec/callables.rst
@@ -71,8 +71,8 @@ may be given as an ellipsis. For example::
   def func(x: AnyStr, y: AnyStr = ...) -> AnyStr: ...
 
 If a non-ellipsis default value is present and its type can be statically
-evaluated, a type checker should verify that this type is compatible with the
-declared parameter's type::
+evaluated, a type checker should verify that this type is :term:`assignable` to
+the declared parameter's type::
 
     def func(x: int = 0): ...  # OK
     def func(x: int | None = None): ...  # OK
@@ -282,8 +282,8 @@ unpacked in the destination callable invocation::
     dest = src      # WRONG!
     dest(**animal)  # Fails at runtime.
 
-Similar situation can happen even without inheritance as compatibility
-between ``TypedDict``\s is based on structural subtyping.
+A similar situation can happen even without inheritance as :term:`assignability
+<assignable>` between ``TypedDict``\s is structural.
 
 Source contains untyped ``**kwargs``
 """"""""""""""""""""""""""""""""""""
@@ -423,11 +423,9 @@ the section on `Callback protocols`_.
 Meaning of ``...`` in ``Callable``
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-The ``Callable`` special form supports the use of ``...`` in place of the
-list of parameter types. This indicates that the type is consistent with
-any input signature. Just as ``Any`` means "any conceivable type that could be
-compatible", ``(...)`` means "any conceivable set of parameters that could be
-compatible"::
+The ``Callable`` special form supports the use of ``...`` in place of the list
+of parameter types. This is a :term:`gradual form` indicating that the type is
+:term:`consistent` with any input signature::
 
     cb1: Callable[..., str]
     cb1 = lambda x: str(x)  # OK
@@ -475,7 +473,7 @@ and are retained as part of the signature::
             pass
 
     class B(A):
-        # This override is OK because it is consistent with the parent's method.
+        # This override is OK because it is assignable to the parent's method.
         def method(self, a: float, /, b: int, *, k: str, m: str) -> None:
             pass
 
@@ -490,7 +488,7 @@ For example::
         f: Callback[...] = cb  # OK
 
 If ``...`` is used with signature concatenation, the ``...`` portion continues
-to mean "any conceivable set of parameters that could be compatible"::
+to be :term:`consistent` with any input parameters::
 
     type CallbackWithInt[**P] = Callable[Concatenate[int, P], str]
     type CallbackWithStr[**P] = Callable[Concatenate[str, P], str]
@@ -522,21 +520,21 @@ and overloads. They can be defined as protocols with a ``__call__`` member::
       ...
 
   comb: Combiner = good_cb  # OK
-  comb = bad_cb  # Error! Argument 2 has incompatible type because of
+  comb = bad_cb  # Error! Argument 2 is not assignable because of
                  # different parameter name and kind in the callback
 
 Callback protocols and ``Callable[...]`` types can generally be used
 interchangeably.
 
 
-Subtyping rules for callables
------------------------------
+Assignability rules for callables
+---------------------------------
 
-A callable type ``A`` is a subtype of callable type ``B`` if the return type
-of ``A`` is a subtype of the return type of ``B`` and the input signature
-of ``A`` accepts all possible combinations of arguments that the input
-signature of ``B`` accepts. All of the specific subtyping rules described below
-derive from this general rule.
+A callable type ``B`` is :term:`assignable` to callable type ``A`` if the
+return type of ``B`` is assignable to the return type of ``A`` and the input
+signature of ``B`` accepts all possible combinations of arguments that the
+input signature of ``A`` accepts. All of the specific assignability rules
+described below derive from this general rule.
 
 
 Parameter types
@@ -544,9 +542,9 @@ Parameter types
 
 Callable types are covariant with respect to their return types but
 contravariant with respect to their parameter types. This means a callable
-``A`` is a subtype of callable ``B`` if the types of the parameters of
-``B`` are subtypes of the parameters of ``A``. For example,
-``(x: float) -> int`` is a subtype of ``(x: int) -> float``::
+``B`` is assignable to callable ``A`` if the types of the parameters of
+``A`` are assignable to the parameters of ``B``. For example,
+``(x: float) -> int`` is assignable to ``(x: int) -> float``::
 
     def func(cb: Callable[[float], int]):
         f1: Callable[[int], float] = cb  # OK
@@ -555,11 +553,11 @@ contravariant with respect to their parameter types. This means a callable
 Parameter kinds
 ^^^^^^^^^^^^^^^
 
-Callable ``A`` is a subtype of callable ``B`` if all keyword-only parameters
-in ``B`` are present in ``A`` as either keyword-only parameters or standard
-(positional or keyword) parameters. For example, ``(a: int) -> None`` is a
-subtype of ``(*, a: int) -> None``, but the converse is not true. The order
-of keyword-only parameters is ignored for purposes of subtyping::
+Callable ``B`` is assignable to callable ``A`` only if all keyword-only
+parameters in ``A`` are present in ``B`` as either keyword-only parameters or
+standard (positional or keyword) parameters. For example, ``(a: int) -> None``
+is assignable to ``(*, a: int) -> None``, but the converse is not true. The
+order of keyword-only parameters is ignored for purposes of assignability::
 
     class KwOnly(Protocol):
         def __call__(self, *, b: int, a: int) -> None: ...
@@ -571,10 +569,10 @@ of keyword-only parameters is ignored for purposes of subtyping::
         f1: KwOnly = standard  # OK
         f2: Standard = kw_only  # Error
 
-Likewise, callable ``A`` is a subtype of callable ``B`` if all positional-only
-parameters in ``B`` are present in ``A`` as either positional-only parameters
-or standard (positional or keyword) parameters. The names of positional-only
-parameters are ignored for purposes of subtyping::
+Likewise, callable ``B`` is assignable to callable ``A`` only if all
+positional-only parameters in ``A`` are present in ``B`` as either
+positional-only parameters or standard (positional or keyword) parameters. The
+names of positional-only parameters are ignored for purposes of assignability::
 
     class PosOnly(Protocol):
         def __call__(self, not_a: int, /) -> None: ...
@@ -590,9 +588,9 @@ parameters are ignored for purposes of subtyping::
 ``*args`` parameters
 ^^^^^^^^^^^^^^^^^^^^
 
-If a callable ``B`` has a signature with a ``*args`` parameter, callable ``A``
-must also have a ``*args`` parameter to be a subtype of ``B``, and the type of
-``B``'s ``*args`` parameter must be a subtype of ``A``'s ``*args`` parameter::
+If a callable ``A`` has a signature with a ``*args`` parameter, callable ``B``
+must also have a ``*args`` parameter to be assignable to ``A``, and the type of
+``A``'s ``*args`` parameter must be assignable to ``B``'s ``*args`` parameter::
 
     class NoArgs(Protocol):
         def __call__(self) -> None: ...
@@ -611,12 +609,12 @@ must also have a ``*args`` parameter to be a subtype of ``B``, and the type of
         f4: IntArgs = float_args  # OK
 
         f5: FloatArgs = no_args  # Error: missing *args parameter
-        f6: FloatArgs = int_args  # Error: float is not subtype of int
+        f6: FloatArgs = int_args  # Error: float is not assignable to int
 
-If a callable ``B`` has a signature with one or more positional-only parameters,
-a callable ``A`` is a subtype of ``B`` if ``A`` has an ``*args`` parameter whose
-type is a supertype of the types of any otherwise-unmatched positional-only
-parameters in ``B``::
+If a callable ``A`` has a signature with one or more positional-only
+parameters, a callable ``B`` is assignable to ``A`` only if ``B`` has an
+``*args`` parameter whose type is assignable from the types of any
+otherwise-unmatched positional-only parameters in ``A``::
 
     class PosOnly(Protocol):
         def __call__(self, a: int, b: str, /) -> None: ...
@@ -634,15 +632,15 @@ parameters in ``B``::
         def __call__(self, a: int, b: str) -> None: ...
 
     def func(int_args: IntArgs, int_str_args: IntStrArgs, str_args: StrArgs):
-        f1: PosOnly = int_args  # Error: str is not subtype of int
+        f1: PosOnly = int_args  # Error: str is not assignable to int
         f2: PosOnly = int_str_args  # OK
         f3: PosOnly = str_args  # OK
-        f4: IntStrArgs = str_args  # Error: int | str is not subtype of str
-        f5: IntStrArgs = int_args  # Error: int | str is not subtype of int
+        f4: IntStrArgs = str_args  # Error: int | str is not assignable to str
+        f5: IntStrArgs = int_args  # Error: int | str is not assignable to int
         f6: StrArgs = int_str_args  # OK
-        f7: StrArgs = int_args  # Error: str is not subtype of int
+        f7: StrArgs = int_args  # Error: str is not assignable to int
         f8: IntArgs = int_str_args  # OK
-        f9: IntArgs = str_args  # Error: int is not subtype of str
+        f9: IntArgs = str_args  # Error: int is not assignable to str
         f10: Standard = int_str_args  # Error: keyword parameters a and b missing
         f11: Standard = str_args  # Error: keyword parameter b missing
 
@@ -650,10 +648,10 @@ parameters in ``B``::
 ``**kwargs`` parameters
 ^^^^^^^^^^^^^^^^^^^^^^^
 
-If a callable ``B`` has a signature with a ``**kwargs`` parameter (without
-an unpacked ``TypedDict`` type annotation), callable ``A`` must also have a
-``**kwargs`` parameter to be a subtype of ``B``, and the type of
-``B``'s ``**kwargs`` parameter must be a subtype of ``A``'s ``**kwargs``
+If a callable ``A`` has a signature with a ``**kwargs`` parameter (without
+an unpacked ``TypedDict`` type annotation), callable ``B`` must also have a
+``**kwargs`` parameter to be assignable to ``A``, and the type of
+``A``'s ``**kwargs`` parameter must be assignable to ``B``'s ``**kwargs``
 parameter::
 
     class NoKwargs(Protocol):
@@ -673,12 +671,12 @@ parameter::
         f4: IntKwargs = float_kwargs  # OK
 
         f5: FloatKwargs = no_kwargs  # Error: missing **kwargs parameter
-        f6: FloatKwargs = int_kwargs  # Error: float is not subtype of int
+        f6: FloatKwargs = int_kwargs  # Error: float is not assignable to int
 
-If a callable ``B`` has a signature with one or more keyword-only parameters,
-a callable ``A`` is a subtype of ``B`` if ``A`` has a ``**kwargs`` parameter
-whose type is a supertype of the types of any otherwise-unmatched keyword-only
-parameters in ``B``::
+If a callable ``A`` has a signature with one or more keyword-only parameters,
+a callable ``B`` is assignable to ``A`` if ``B`` has a ``**kwargs`` parameter
+whose type is assignable from the types of any otherwise-unmatched keyword-only
+parameters in ``A``::
 
     class KwOnly(Protocol):
         def __call__(self, *, a: int, b: str) -> None: ...
@@ -696,19 +694,19 @@ parameters in ``B``::
         def __call__(self, a: int, b: str) -> None: ...
 
     def func(int_kwargs: IntKwargs, int_str_kwargs: IntStrKwargs, str_kwargs: StrKwargs):
-        f1: KwOnly = int_kwargs  # Error: str is not subtype of int
+        f1: KwOnly = int_kwargs  # Error: str is not assignable to int
         f2: KwOnly = int_str_kwargs  # OK
         f3: KwOnly = str_kwargs  # OK
-        f4: IntStrKwargs = str_kwargs  # Error: int | str is not subtype of str
-        f5: IntStrKwargs = int_kwargs  # Error: int | str is not subtype of int
+        f4: IntStrKwargs = str_kwargs  # Error: int | str is not assignable to str
+        f5: IntStrKwargs = int_kwargs  # Error: int | str is not assignable to int
         f6: StrKwargs = int_str_kwargs  # OK
-        f7: StrKwargs = int_kwargs  # Error: str is not subtype of int
+        f7: StrKwargs = int_kwargs  # Error: str is not assignable to int
         f8: IntKwargs = int_str_kwargs  # OK
-        f9: IntKwargs = str_kwargs  # Error: int is not subtype of str
+        f9: IntKwargs = str_kwargs  # Error: int is not assignable to str
         f10: Standard = int_str_kwargs  # Error: Does not accept positional arguments
         f11: Standard = str_kwargs  # Error: Does not accept positional arguments
 
-Subtyping relationships for callable signatures that contain a ``**kwargs``
+Assignability relationships for callable signatures that contain a ``**kwargs``
 with an unpacked ``TypedDict`` are described in the section :ref:`above <unpack-kwargs>`.
 
 
@@ -732,10 +730,10 @@ to a ``Callable`` parameterized by ``P``::
 Default argument values
 ^^^^^^^^^^^^^^^^^^^^^^^
 
-If a callable ``A`` has a parameter ``x`` with a default argument value and
-``B`` is the same as ``A`` except that ``x`` has no default argument, then
-``A`` is a subtype of ``B``. ``A`` is also a subtype of ``C``
-if ``C`` is the same as ``A`` with parameter ``x`` removed::
+If a callable ``C`` has a parameter ``x`` with a default argument value and
+``A`` is the same as ``C`` except that ``x`` has no default argument, then
+``C`` is assignable to ``A``. ``C`` is also assignable to ``A``
+if ``A`` is the same as ``C`` with parameter ``x`` removed::
 
     class DefaultArg(Protocol):
         def __call__(self, x: int = 0) -> None: ...
@@ -754,9 +752,9 @@ if ``C`` is the same as ``A`` with parameter ``x`` removed::
 Overloads
 ^^^^^^^^^
 
-If a callable ``A`` is overloaded with two or more signatures, it is a subtype
-of callable ``B`` if *at least one* of the overloaded signatures in ``A`` is
-a subtype of ``B``::
+If a callable ``B`` is overloaded with two or more signatures, it is assignable
+to callable ``A`` if *at least one* of the overloaded signatures in ``B`` is
+assignable to ``A``::
 
     class Overloaded(Protocol):
         @overload
@@ -778,8 +776,9 @@ a subtype of ``B``::
         f2: StrArg = overloaded  # OK
         f3: FloatArg = overloaded  # Error
 
-If a callable ``B`` is overloaded with two or more signatures, callable ``A``
-is a subtype of ``B`` if ``A`` is a subtype of *all* of the signatures in ``B``::
+If a callable ``A`` is overloaded with two or more signatures, callable ``B``
+is assignable to ``A`` if ``B`` is assignable to *all* of the signatures in
+``A``::
 
     class Overloaded(Protocol):
         @overload
diff --git a/docs/spec/class-compat.rst b/docs/spec/class-compat.rst
index b49a2034..c1f47ffb 100644
--- a/docs/spec/class-compat.rst
+++ b/docs/spec/class-compat.rst
@@ -1,6 +1,6 @@
 .. _`class-compat`:
 
-Class type compatibility
+Class type assignability
 ========================
 
 .. _`classvar`:
@@ -97,8 +97,9 @@ annotated in ``__init__`` or other methods, rather than in the class::
 (Originally specified by :pep:`698`.)
 
 When type checkers encounter a method decorated with ``@typing.override`` they
-should treat it as a type error unless that method is overriding a compatible
-method or attribute in some ancestor class.
+should treat it as a type error unless that method is overriding a method or
+attribute in some ancestor class, and the type of the overriding method is
+assignable to the type of the overridden method.
 
 
 .. code-block:: python
diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst
index c924fefa..7d2a48ff 100644
--- a/docs/spec/concepts.rst
+++ b/docs/spec/concepts.rst
@@ -66,6 +66,10 @@ or a class that inherits directly or indirectly from ``str``. A :ref:`Protocol
 <Protocols>` denotes the set of all objects which share a certain set of
 attributes and/or methods.
 
+If an object ``v`` is a member of the set of objects denoted by a fully static
+type ``T``, we can say that ``v`` is a "member of" the type ``T``, or ``v``
+"inhabits" ``T``.
+
 Gradual types
 ~~~~~~~~~~~~~
 
@@ -182,6 +186,8 @@ static" type than ``A``, and ``A`` is a "more dynamic" type than ``B``.
 The materialization relation is both transitive and reflexive, so it defines a
 preorder on gradual types.
 
+.. _`consistent`:
+
 Consistency
 -----------
 
@@ -208,6 +214,8 @@ The consistency relation is symmetric. If ``A`` is consistent with ``B``, ``B``
 is also consistent with ``A``. It is also reflexive: ``A`` is always consistent
 with ``A``.
 
+.. _`assignable`:
+
 The assignable-to (or consistent subtyping) relation
 ----------------------------------------------------
 
diff --git a/docs/spec/constructors.rst b/docs/spec/constructors.rst
index 0eb34b84..547d736f 100644
--- a/docs/spec/constructors.rst
+++ b/docs/spec/constructors.rst
@@ -105,11 +105,11 @@ unrelated class.
 
 If the evaluated return type of ``__new__`` is not the class being constructed
 (or a subclass thereof), a type checker should assume that the ``__init__``
-method will not be called. This is consistent with the runtime behavior of
-the ``type.__call__`` method. If the ``__new__`` method return type is
-a union with one or more subtypes that are not instances of the class being
-constructed (or a subclass thereof), a type checker should likewise assume that
-the ``__init__`` method will not be called.
+method will not be called. This is consistent with the runtime behavior of the
+``type.__call__`` method. If the ``__new__`` method return type is a union with
+one or more members that are not the class being constructed (or a subclass
+thereof), a type checker should likewise assume that the ``__init__`` method
+will not be called.
 
   ::
 
@@ -337,7 +337,7 @@ Consistency of ``__new__`` and ``__init__``
 -------------------------------------------
 
 Type checkers may optionally validate that the ``__new__`` and ``__init__``
-methods for a class have consistent signatures.
+methods for a class have :term:`consistent` signatures.
 
   ::
 
@@ -353,7 +353,8 @@ methods for a class have consistent signatures.
 Converting a Constructor to Callable
 ------------------------------------
 
-Class objects are callable, which means they are compatible with callable types.
+Class objects are callable, which means they are :term:`assignable` to callable
+types.
 
   ::
 
diff --git a/docs/spec/directives.rst b/docs/spec/directives.rst
index 01c0f6bd..7fca698a 100644
--- a/docs/spec/directives.rst
+++ b/docs/spec/directives.rst
@@ -86,12 +86,6 @@ At runtime a cast always returns the
 expression unchanged -- it does not check the type, and it does not
 convert or coerce the value.
 
-Casts differ from type comments (see the previous section).  When using
-a type comment, the type checker should still verify that the inferred
-type is consistent with the stated type.  When using a cast, the type
-checker should blindly believe the programmer.  Also, casts can be used
-in expressions, while type comments only apply to assignments.
-
 .. _`if-type-checking`:
 
 ``TYPE_CHECKING``
diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst
index 53d8626f..b87641d9 100644
--- a/docs/spec/generics.rst
+++ b/docs/spec/generics.rst
@@ -479,7 +479,7 @@ using the ``TypeVar`` constructor) or using ``: <type>`` (when using the native
 syntax for generics). The bound itself cannot be parameterized by type variables.
 This means that an
 actual type substituted (explicitly or implicitly) for the type variable must
-be a subtype of the boundary type. Example::
+be :term:`assignable` to the boundary type. Example::
 
   from typing import TypeVar
   from collections.abc import Sized
@@ -496,11 +496,10 @@ be a subtype of the boundary type. Example::
   longer({1}, {1, 2})  # ok, return type set[int]
   longer([1], {1, 2})  # ok, return type a supertype of list[int] and set[int]
 
-An upper bound cannot be combined with type constraints (as used in
-``AnyStr``, see the example earlier); type constraints cause the
-inferred type to be *exactly* one of the constraint types, while an
-upper bound just requires that the actual type is a subtype of the
-boundary type.
+An upper bound cannot be combined with type constraints (as used in ``AnyStr``,
+see the example earlier); type constraints cause the inferred type to be
+*exactly* one of the constraint types, while an upper bound just requires that
+the actual type is :term:`assignable` to the boundary type.
 
 .. _`variance`:
 
@@ -523,13 +522,12 @@ introduction to these concepts can be found on `Wikipedia
 <https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29>`_ and in :pep:`483`; here we just show how to control
 a type checker's behavior.
 
-By default generic types declared using the old ``TypeVar`` syntax
-are considered *invariant* in all type variables,
-which means that values for variables annotated with types like
-``list[Employee]`` must exactly match the type annotation -- no subclasses or
-superclasses of the type parameter (in this example ``Employee``) are
-allowed. See below for the behavior when using the built-in generic syntax
-in Python 3.12 and higher.
+By default generic types declared using the old ``TypeVar`` syntax are
+considered *invariant* in all type variables, which means that e.g.
+``list[Manager]`` is neither a supertype nor a subtype of ``list[Employee]``.
+
+See below for the behavior when using the built-in generic syntax in Python
+3.12 and higher.
 
 To facilitate the declaration of container types where covariant or
 contravariant type checking is acceptable, type variables accept keyword
@@ -1926,7 +1924,7 @@ Using a type parameter from an outer scope as a default is not supported.
 Bound Rules
 ^^^^^^^^^^^
 
-``T1``'s bound must be a subtype of ``T2``'s bound.
+``T1``'s bound must be a :term:`consistent subtype` of ``T2``'s bound.
 
 ::
 
@@ -2023,8 +2021,8 @@ Using ``bound`` and ``default``
 """""""""""""""""""""""""""""""
 
 If both ``bound`` and ``default`` are passed, ``default`` must be a
-subtype of ``bound``. If not, the type checker should generate an
-error.
+:term:`consistent subtype` of ``bound``. If not, the type checker should
+generate an error.
 
 ::
 
@@ -2268,7 +2266,8 @@ Use in Attribute Annotations
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Another use for ``Self`` is to annotate attributes. One example is where we
-have a ``LinkedList`` whose elements must be subclasses of the current class.
+have a ``LinkedList`` whose elements must be consistent subtypes of the current
+class.
 
 ::
 
@@ -2298,8 +2297,8 @@ constructions with subclasses:
         def ordinal_value(self) -> str:
             return as_ordinal(self.value)
 
-    # Should not be OK because LinkedList[int] is not a subclass of
-    # OrdinalLinkedList, # but the type checker allows it.
+    # Should not be OK because LinkedList[int] is not a consistent subtype of
+    # OrdinalLinkedList, but the type checker allows it.
     xs = OrdinalLinkedList(value=1, next=LinkedList[int](value=2))
 
     if xs.next:
@@ -2469,11 +2468,10 @@ See :pep:`PEP 544
 <544#self-types-in-protocols>` for
 details on the behavior of TypeVars bound to protocols.
 
-Checking a class for compatibility with a protocol: If a protocol uses
-``Self`` in methods or attribute annotations, then a class ``Foo`` is
-considered compatible with the protocol if its corresponding methods and
-attribute annotations use either ``Self`` or ``Foo`` or any of ``Foo``’s
-subclasses. See the examples below:
+Checking a class for assignability to a protocol: If a protocol uses ``Self``
+in methods or attribute annotations, then a class ``Foo`` is assignable to the
+protocol if its corresponding methods and attribute annotations use either
+``Self`` or ``Foo`` or any of ``Foo``’s subclasses. See the examples below:
 
 ::
 
@@ -2705,16 +2703,15 @@ by the ``TypeVar`` constructor call. No further inference is needed.
 3. Create two specialized versions of the class. We'll refer to these as
 ``upper`` and ``lower`` specializations. In both of these specializations,
 replace all type parameters other than the one being inferred by a dummy type
-instance (a concrete anonymous class that is type compatible with itself and
-assumed to meet the bounds or constraints of the type parameter). In
-the ``upper`` specialized class, specialize the target type parameter with
-an ``object`` instance. This specialization ignores the type parameter's
-upper bound or constraints. In the ``lower`` specialized class, specialize
-the target type parameter with itself (i.e. the corresponding type argument
-is the type parameter itself).
-
-4. Determine whether ``lower`` can be assigned to ``upper`` using normal type
-compatibility rules. If so, the target type parameter is covariant. If not,
+instance (a concrete anonymous class that is assumed to meet the bounds or
+constraints of the type parameter). In the ``upper`` specialized class,
+specialize the target type parameter with an ``object`` instance. This
+specialization ignores the type parameter's upper bound or constraints. In the
+``lower`` specialized class, specialize the target type parameter with itself
+(i.e. the corresponding type argument is the type parameter itself).
+
+4. Determine whether ``lower`` can be assigned to ``upper`` using normal
+assignability rules. If so, the target type parameter is covariant. If not,
 determine whether ``upper`` can be assigned to ``lower``. If so, the target
 type parameter is contravariant. If neither of these combinations are
 assignable, the target type parameter is invariant.
@@ -2737,9 +2734,8 @@ To determine the variance of ``T1``, we specialize ``ClassA`` as follows:
     upper = ClassA[object, Dummy, Dummy]
     lower = ClassA[T1, Dummy, Dummy]
 
-We find that ``upper`` is not assignable to ``lower`` using normal type
-compatibility rules defined in :pep:`484`. Likewise, ``lower`` is not assignable
-to ``upper``, so we conclude that ``T1`` is invariant.
+We find that ``upper`` is not assignable to ``lower``. Likewise, ``lower`` is
+not assignable to ``upper``, so we conclude that ``T1`` is invariant.
 
 To determine the variance of ``T2``, we specialize ``ClassA`` as follows:
 
diff --git a/docs/spec/literal.rst b/docs/spec/literal.rst
index d0ca618c..ac4552c0 100644
--- a/docs/spec/literal.rst
+++ b/docs/spec/literal.rst
@@ -24,9 +24,8 @@ concrete value. For example, if we define some variable ``foo`` to have
 type ``Literal[3]``, we are declaring that ``foo`` must be exactly equal
 to ``3`` and no other value.
 
-Given some value ``v`` that is a member of type ``T``, the type
-``Literal[v]`` shall be treated as a subtype of ``T``. For example,
-``Literal[3]`` is a subtype of ``int``.
+Given some value ``v`` that is a member of type ``T``, the type ``Literal[v]``
+is a subtype of ``T``. For example, ``Literal[3]`` is a subtype of ``int``.
 
 All methods from the parent type will be directly inherited by the
 literal type. So, if we have some variable ``foo`` of type ``Literal[3]``
@@ -304,13 +303,13 @@ special-casing. For example, programs like the following are type safe::
    # Legal: Literal["foo"] is a subtype of str
    expects_str(var)
 
-This also means non-Literal expressions in general should not automatically
-be cast to Literal. For example::
+This also means non-Literal types in general are not assignable to Literal
+types. For example::
 
    def expects_literal(x: Literal["foo"]) -> None: ...
 
    def runner(my_str: str) -> None:
-       # ILLEGAL: str is not a subclass of Literal["foo"]
+       # ILLEGAL: str is not assignable to Literal["foo"]
        expects_literal(my_str)
 
 **Note:** If the user wants their API to support accepting both literals
@@ -398,9 +397,8 @@ maintain backwards-compatibility.
 Interactions with generics
 """"""""""""""""""""""""""
 
-Types like ``Literal[3]`` are meant to be just plain old subclasses of
-``int``. This means you can use types like ``Literal[3]`` anywhere
-you could use normal types, such as with generics.
+Since a type like ``Literal[3]`` is a subtype of ``int``, you can use
+``Literal[3]`` anywhere you could use ``int``, such as with generics.
 
 This means that it is legal to parameterize generic functions or
 classes using Literal types::
@@ -584,7 +582,7 @@ Type inference
 Inferring ``LiteralString``
 """""""""""""""""""""""""""
 
-Any literal string type is compatible with ``LiteralString``. For
+Any literal string type is assignable to ``LiteralString``. For
 example, ``x: LiteralString = "foo"`` is valid because ``"foo"`` is
 inferred to be of type ``Literal["foo"]``.
 
@@ -592,20 +590,20 @@ We also infer ``LiteralString`` in the
 following cases:
 
 + Addition: ``x + y`` is of type ``LiteralString`` if both ``x`` and
-  ``y`` are compatible with ``LiteralString``.
+  ``y`` are assignable to ``LiteralString``.
 
 + Joining: ``sep.join(xs)`` is of type ``LiteralString`` if ``sep``'s
-  type is compatible with ``LiteralString`` and ``xs``'s type is
-  compatible with ``Iterable[LiteralString]``.
+  type is assignable to ``LiteralString`` and ``xs``'s type is
+  assignable to ``Iterable[LiteralString]``.
 
 + In-place addition: If ``s`` has type ``LiteralString`` and ``x`` has
-  type compatible with ``LiteralString``, then ``s += x`` preserves
+  type assignable to ``LiteralString``, then ``s += x`` preserves
   ``s``'s type as ``LiteralString``.
 
-+ String formatting: An f-string has type ``LiteralString`` if and only
-  if its constituent expressions are literal strings. ``s.format(...)``
-  has type ``LiteralString`` if and only if ``s`` and the arguments have
-  types compatible with ``LiteralString``.
++ String formatting: An f-string has type ``LiteralString`` if and only if its
+  constituent expressions are literal strings. ``s.format(...)`` is assignable
+  to ``LiteralString`` if and only if ``s`` and the arguments have types
+  assignable to ``LiteralString``.
 
 In all other cases, if one or more of the composed values has a
 non-literal type ``str``, the composition of types will have type
@@ -613,7 +611,7 @@ non-literal type ``str``, the composition of types will have type
 has type ``str``. This matches the pre-existing behavior of type
 checkers.
 
-``LiteralString`` is compatible with the type ``str``. It inherits all
+``LiteralString`` is assignable to the type ``str``. It inherits all
 methods from ``str``. So, if we have a variable ``s`` of type
 ``LiteralString``, it is safe to write ``s.startswith("hello")``.
 
@@ -626,7 +624,7 @@ check:
         if s == "bar":
             reveal_type(s)  # => Literal["bar"]
 
-Such a refined type in the if-block is also compatible with
+Such a refined type in the if-block is also assignable to
 ``LiteralString`` because its type is ``Literal["bar"]``.
 
 
@@ -699,7 +697,7 @@ Format strings using literal strings:
 
     expect_literal_string("hello {}".format(username))  # Not OK
 
-Other literal types, such as literal integers, are not compatible with ``LiteralString``:
+Other literal types, such as literal integers, are not assignable to ``LiteralString``:
 
 ::
 
diff --git a/docs/spec/namedtuples.rst b/docs/spec/namedtuples.rst
index 835d196f..1ac14136 100644
--- a/docs/spec/namedtuples.rst
+++ b/docs/spec/namedtuples.rst
@@ -133,11 +133,12 @@ this::
     x, y = p  # Type error (too few values to unpack)
 
 
-Type Compatibility Rules
-------------------------
+Assignability
+-------------
 
-A named tuple is a subtype of a ``tuple`` with a known length and parameterized
-by types corresponding to the named tuple's individual field types::
+A named tuple is :term:`assignable` to a ``tuple`` with a known length and
+parameterized by types corresponding to the named tuple's individual field
+types::
 
     p = Point(x=1, y=2, units="inches")
     v1: tuple[int, int, str] = p  # OK
diff --git a/docs/spec/narrowing.rst b/docs/spec/narrowing.rst
index cbab74f0..b7c6cc0d 100644
--- a/docs/spec/narrowing.rst
+++ b/docs/spec/narrowing.rst
@@ -149,8 +149,8 @@ To specify the behavior of ``TypeIs``, we use the following terminology:
         else:
             assert_type(val, NN)
 
-The return type ``R`` must be consistent with ``I``. The type checker should
-emit an error if this condition is not met.
+The return type ``R`` must be :term:`assignable` to ``I``. The type checker
+should emit an error if this condition is not met.
 
 Formally, type *NP* should be narrowed to :math:`A \land R`,
 the intersection of *A* and *R*, and type *NN* should be narrowed to
@@ -193,7 +193,8 @@ argument's previously-known type::
         else:
             assert_type(x, int)
 
-It is an error to narrow to a type that is not consistent with the input type::
+It is an error to narrow to a type that is not :term:`assignable` to the input
+type::
 
     from typing import TypeIs
 
diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst
index 5532276f..e6b39ad8 100644
--- a/docs/spec/protocol.rst
+++ b/docs/spec/protocol.rst
@@ -22,19 +22,17 @@ The distinction is not important most of the time, and in other
 cases we can just add a qualifier such as *protocol classes*
 when referring to the static type concept.
 
-If a class includes a protocol in its MRO, the class is called
-an *explicit* subclass of the protocol. If a class is a structural subtype
-of a protocol, it is said to implement the protocol and to be compatible
-with a protocol. If a class is compatible with a protocol but the protocol
-is not included in the MRO, the class is an *implicit* subtype
-of the protocol. (Note that one can explicitly subclass a protocol and
-still not implement it if a protocol attribute is set to ``None``
-in the subclass, see Python :py:ref:`data model <specialnames>`
-for details.)
-
-The attributes (variables and methods) of a protocol that are mandatory
-for another class in order to be considered a structural subtype are called
-protocol members.
+If a class includes a protocol in its MRO, the class is called an *explicit*
+subclass of the protocol. If a class is a structural consistent subtype of a
+protocol, it is said to implement the protocol and to be assignable to the
+protocol. If a class is assignable to a protocol but the protocol is not
+included in the MRO, the class is *implicitly* assignable to the protocol.
+(Note that one can explicitly subclass a protocol and still not implement it if
+a protocol attribute is set to ``None`` in the subclass, see Python
+:py:ref:`data model <specialnames>` for details.)
+
+The attributes (variables and methods) of a protocol that are mandatory for
+another class to be assignable to the protocol are called protocol members.
 
 .. _protocol-definition:
 
@@ -51,9 +49,9 @@ at the end of the list. Here is a simple example::
       def close(self) -> None:
           ...
 
-Now if one defines a class ``Resource`` with a ``close()`` method that has
-a compatible signature, it would implicitly be a subtype of
-``SupportsClose``, since the structural subtyping is used for
+Now if one defines a class ``Resource`` with a ``close()`` method whose type
+signature is assignable to ``SupportsClose.close``, it would implicitly be
+assignable to ``SupportsClose``, since structural assignability is used for
 protocol types::
 
   class Resource:
@@ -74,10 +72,9 @@ be used in every context where normal types can::
   close_all([f, r])  # OK!
   close_all([1])     # Error: 'int' has no 'close' method
 
-Note that both the user-defined class ``Resource`` and the built-in
-``IO`` type (the return type of ``open()``) are considered subtypes of
-``SupportsClose``, because they provide a ``close()`` method with
-a compatible type signature.
+Note that both the user-defined class ``Resource`` and the built-in ``IO`` type
+(the return type of ``open()``) are assignable to ``SupportsClose``, because
+they provide a ``close()`` method with an assignable type signature.
 
 
 Protocol members
@@ -147,9 +144,9 @@ expected to automatically detect that a class implements a given protocol.
 So while it's possible to subclass a protocol explicitly, it's *not necessary*
 to do so for the sake of type-checking.
 
-The default implementations cannot be used if
-the subtype relationship is implicit and only via structural
-subtyping -- the semantics of inheritance is not changed. Examples::
+The default implementations cannot be used if the assignable-to relationship is
+implicit and only structural -- the semantics of inheritance is not changed.
+Examples::
 
     class PColor(Protocol):
         @abstractmethod
@@ -181,10 +178,10 @@ subtyping -- the semantics of inheritance is not changed. Examples::
     represent(nice) # OK
     represent(another) # Also OK
 
-Note that there is little difference between explicit and implicit
+Note that there is little difference between explicit and implicit consistent
 subtypes; the main benefit of explicit subclassing is to get some protocol
-methods "for free". In addition, type checkers can statically verify that
-the class actually implements the protocol correctly::
+methods "for free". In addition, type checkers can statically verify that the
+class actually implements the protocol correctly::
 
     class RGB(Protocol):
         rgb: tuple[int, int, int]
@@ -201,9 +198,9 @@ the class actually implements the protocol correctly::
 
 A class can explicitly inherit from multiple protocols and also from normal
 classes. In this case methods are resolved using normal MRO and a type checker
-verifies that all subtyping are correct. The semantics of ``@abstractmethod``
-is not changed; all of them must be implemented by an explicit subclass
-before it can be instantiated.
+verifies that all member assignability is correct. The semantics of
+``@abstractmethod`` is not changed; all of them must be implemented by an
+explicit subclass before it can be instantiated.
 
 
 Merging and extending protocols
@@ -248,7 +245,7 @@ with ``typing.Sized``::
 
 The two definitions of ``SizedAndClosable`` are equivalent.
 Subclass relationships between protocols are not meaningful when
-considering subtyping, since structural compatibility is
+considering assignability, since structural assignability is
 the criterion, not the MRO.
 
 If ``Protocol`` is included in the base class list, all the other base classes
@@ -303,7 +300,7 @@ the declared variance. Examples::
 
   var: Proto[float]
   another_var: Proto[int]
-  var = another_var  # Error! 'Proto[float]' is incompatible with 'Proto[int]'.
+  var = another_var  # Error! 'Proto[float]' is not assignable to 'Proto[int]'.
 
 Note that unlike nominal classes, de facto covariant protocols cannot be
 declared as invariant, since this can break transitivity of subtyping.
@@ -328,7 +325,7 @@ like trees in an abstract fashion::
       def leaves(self) -> Iterable['Traversable']:
           ...
 
-Note that for recursive protocols, a class is considered a subtype of
+Note that for recursive protocols, a class is considered assignable to
 the protocol in situations where the decision depends on itself.
 Continuing the previous example::
 
@@ -345,7 +342,7 @@ Continuing the previous example::
   def walk(graph: Traversable) -> None:
       ...
   tree: Tree[float] = Tree()
-  walk(tree)  # OK, 'Tree[float]' is a subtype of 'Traversable'
+  walk(tree)  # OK, 'Tree[float]' is assignable to 'Traversable'
 
 
 Self-types in protocols
@@ -371,26 +368,26 @@ The self-types in protocols follow the
   c = One()  # OK
   c = Other()  # Also OK
 
-Subtyping relationships with other types
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Assignability relationships with other types
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Protocols cannot be instantiated, so there are no values whose
 runtime type is a protocol. For variables and parameters with protocol types,
-subtyping relationships are subject to the following rules:
+assignability relationships are subject to the following rules:
 
-* A protocol is never a subtype of a concrete type.
-* A concrete type ``X`` is a subtype of protocol ``P``
+* A protocol is never assignable to a concrete type.
+* A concrete type ``X`` is assignable to a protocol ``P``
   if and only if ``X`` implements all protocol members of ``P`` with
-  compatible types. In other words, subtyping with respect to a protocol is
+  assignable types. In other words, assignability with respect to a protocol is
   always structural.
-* A protocol ``P1`` is a subtype of another protocol ``P2`` if ``P1`` defines
-  all protocol members of ``P2`` with compatible types.
+* A protocol ``P1`` is assignable to another protocol ``P2`` if ``P1`` defines
+  all protocol members of ``P2`` with assignable types.
 
 Generic protocol types follow the same rules of variance as non-protocol
 types. Protocol types can be used in all contexts where any other types
 can be used, such as in unions, ``ClassVar``, type variables bounds, etc.
 Generic protocols follow the rules for generic abstract classes, except for
-using structural compatibility instead of compatibility defined by
+using structural assignability instead of assignability defined by
 inheritance relationships.
 
 Static type checkers will recognize protocol implementations, even if the
@@ -460,8 +457,8 @@ Example::
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Variables and parameters annotated with ``type[Proto]`` accept only concrete
-(non-protocol) subtypes of ``Proto``. The main reason for this is to allow
-instantiation of parameters with such types. For example::
+(non-protocol) consistent subtypes of ``Proto``. The main reason for this is to
+allow instantiation of parameters with such types. For example::
 
   class Proto(Protocol):
       @abstractmethod
@@ -489,7 +486,7 @@ For normal (non-abstract) classes, the behavior of ``type[]`` is
 not changed.
 
 A class object is considered an implementation of a protocol if accessing
-all members on it results in types compatible with the protocol members.
+all members on it results in types assignable to the types of the protocol members.
 For example::
 
   from typing import Any, Protocol
@@ -538,7 +535,7 @@ Modules as implementations of protocols
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 A module object is accepted where a protocol is expected if the public
-interface of the given module is compatible with the expected protocol.
+interface of the given module is assignable to the expected protocol.
 For example::
 
   # file default_config.py
@@ -560,7 +557,7 @@ For example::
 
   setup(default_config)  # OK
 
-To determine compatibility of module level functions, the ``self`` argument
+To determine assignability of module level functions, the ``self`` argument
 of the corresponding protocol methods is dropped. For example::
 
   # callbacks.py
@@ -622,11 +619,11 @@ the risks for this feature, the following rules are applied.
   if it only contains methods as members (for example ``Sized``,
   ``Iterator``, etc). A protocol that contains at least one non-method member
   (like ``x: int``) is called a data protocol.
-* *Unsafe overlap*: A type ``X`` is called unsafely overlapping with
-  a protocol ``P``, if ``X`` is not a subtype of ``P``, but it is a subtype
-  of the type erased version of ``P`` where all members have type ``Any``.
-  In addition, if at least one element of a union unsafely overlaps with
-  a protocol ``P``, then the whole union is unsafely overlapping with ``P``.
+* *Unsafe overlap*: A type ``X`` is called unsafely overlapping with a protocol
+  ``P``, if ``X`` is not assignable to ``P``, but it is assignable to the type
+  erased version of ``P`` where all members have type ``Any``. In addition, if
+  at least one element of a union unsafely overlaps with a protocol ``P``, then
+  the whole union is unsafely overlapping with ``P``.
 
 **Specification**:
 
diff --git a/docs/spec/qualifiers.rst b/docs/spec/qualifiers.rst
index 49ec63f2..13cd842b 100644
--- a/docs/spec/qualifiers.rst
+++ b/docs/spec/qualifiers.rst
@@ -255,7 +255,7 @@ details of the syntax:
 
     V == Annotated[list[tuple[int, int]], MaxLen(10)]
 
-* As with most :term:`special forms <special form>`, ``Annotated`` is not type compatible with
+* As with most :term:`special forms <special form>`, ``Annotated`` is not assignable to
   ``type`` or ``type[T]``::
 
     v1: type[int] = Annotated[int, ""]  # Type error
diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst
index 985ffeca..46e1f2bf 100644
--- a/docs/spec/special-types.rst
+++ b/docs/spec/special-types.rst
@@ -10,7 +10,8 @@ Special types in annotations
 
 ``Any`` represents an unknown static type.
 
-Every type is assignable to ``Any``, and ``Any`` is assignable to every type.
+Every type is :term:`assignable` to ``Any``, and ``Any`` is assignable to every
+type.
 
 See :ref:`type-system-concepts` for more discussion of ``Any``.
 
@@ -93,8 +94,9 @@ is unreachable and will behave accordingly::
 ``Never``
 ---------
 
-Since Python 3.11, the ``typing`` module contains a :term:`special form` ``Never``. It
-represents the bottom type, a type that has no members.
+Since Python 3.11, the ``typing`` module contains a :term:`special form`
+``Never``. It represents the bottom type, a type that represents the empty set
+of Python objects.
 
 The ``Never`` type is equivalent to ``NoReturn``, which is discussed above.
 The ``NoReturn`` type is conventionally used in return annotations of
diff --git a/docs/spec/tuples.rst b/docs/spec/tuples.rst
index 4f04b914..1209cc02 100644
--- a/docs/spec/tuples.rst
+++ b/docs/spec/tuples.rst
@@ -29,10 +29,10 @@ Arbitrary-length homogeneous tuples are sometimes referred to as "unbounded
 tuples". Both of these terms appear within the typing spec, and they refer to
 the same concept.
 
-The type ``tuple[Any, ...]`` is special in that it is bidirectionally
-compatible with any tuple of any length. This is useful for gradual typing.
-The type ``tuple`` (with no type arguments provided) is equivalent to
-``tuple[Any, ...]``.
+The type ``tuple[Any, ...]`` is special in that it is :term:`consistent` with
+all tuple types, and :term:`assignable` to a tuple of any length. This is
+useful for gradual typing. The type ``tuple`` (with no type arguments provided)
+is equivalent to ``tuple[Any, ...]``.
 
 Arbitrary-length tuples have exactly two type arguments -- the type and
 an ellipsis. Any other tuple form that uses an ellipsis is invalid::
@@ -61,8 +61,7 @@ more elements of type ``str``. The type ``tuple[*tuple[int, ...]]`` is
 equivalent to ``tuple[int, ...]``.
 
 If an unpacked ``*tuple[Any, ...]`` is embedded within another tuple, that
-portion of the tuple is bidirectionally type compatible with any tuple of
-any length.
+portion of the tuple is :term:`consistent` with any tuple of any length.
 
 Only one unbounded tuple can be used within another tuple::
 
@@ -100,7 +99,7 @@ to a union of tuples of different lengths. That means ``tuple[()]``,
 ``tuple[int, ...]``. The converse is not true; ``tuple[int, ...]`` is not a
 subtype of ``tuple[int]``.
 
-The type ``tuple[Any, ...]`` is bidirectionally compatible with any tuple::
+The type ``tuple[Any, ...]`` is :term:`consistent` with any tuple::
 
     def func(t1: tuple[int], t2: tuple[int, ...], t3: tuple[Any, ...]):
         v1: tuple[int, ...] = t1  # OK
diff --git a/docs/spec/typeddict.rst b/docs/spec/typeddict.rst
index 6d632655..2903c040 100644
--- a/docs/spec/typeddict.rst
+++ b/docs/spec/typeddict.rst
@@ -27,13 +27,13 @@ supported by ``typing.NamedTuple``.  Other features include
 TypedDict inheritance and totality (specifying whether keys are
 required or not).
 
-This section also provides a sketch of how a type checker is expected
-to support type checking operations involving TypedDict objects.
-Similar to :pep:`484`, this discussion is left somewhat vague on purpose,
-to allow experimentation with a wide variety of different type
-checking approaches.  In particular, type compatibility should be
-based on structural compatibility: a more specific TypedDict type can
-be compatible with a smaller (more general) TypedDict type.
+This section also provides a sketch of how a type checker is expected to
+support type checking operations involving TypedDict objects. Similar to
+:pep:`484`, this discussion is left somewhat vague on purpose, to allow
+experimentation with a wide variety of different type checking approaches.  In
+particular, :term:`assignability <assignable>` should be structural: a more
+specific TypedDict type can be assignable to a smaller (more general)
+TypedDict type.
 
 
 Class-based Syntax
@@ -284,24 +284,16 @@ refers to a dictionary object does not need to be supported, to simplify
 implementation.
 
 
-Type Consistency
-^^^^^^^^^^^^^^^^
+Assignability
+^^^^^^^^^^^^^
 
-Informally speaking, *type consistency* is a generalization of the
-is-subtype-of relation to support the ``Any`` type.  It is defined
-more formally in :pep:`483`.  This section introduces the
-new, non-trivial rules needed to support type consistency for
-TypedDict types.
+First, any TypedDict type is :term:`assignable` to ``Mapping[str, object]``.
 
-First, any TypedDict type is consistent with ``Mapping[str, object]``.
-Second, a TypedDict type ``A`` is consistent with TypedDict ``B`` if
-``A`` is structurally compatible with ``B``.  This is true if and only
-if both of these conditions are satisfied:
+Second, a TypedDict type ``B`` is :term:`assignable` to a TypedDict ``A`` if
+and only if both of these conditions are satisfied:
 
-* For each key in ``B``, ``A`` has the corresponding key and the
-  corresponding value type in ``A`` is consistent with the value type
-  in ``B``.  For each key in ``B``, the value type in ``B`` is also
-  consistent with the corresponding value type in ``A``.
+* For each key in ``A``, ``B`` has the corresponding key and the corresponding
+  value type in ``B`` is :term:`consistent` with the value type in ``A``.
 
 * For each required key in ``B``, the corresponding key is required
   in ``A``.  For each non-required key in ``B``, the corresponding key
@@ -323,7 +315,7 @@ Discussion:
           a['x'] = None
 
       b: B = {'x': 0}
-      f(b)  # Type check error: 'B' not compatible with 'A'
+      f(b)  # Type check error: 'B' not assignable to 'A'
       b['x'] + 1  # Runtime error: None + 1
 
 * A TypedDict type with a required key is not consistent with a