diff --git a/peps/pep-0747.rst b/peps/pep-0747.rst
index e4ce2a0ee65..50ed2f723f7 100644
--- a/peps/pep-0747.rst
+++ b/peps/pep-0747.rst
@@ -200,11 +200,15 @@ that represent a type assignable to ``str | None``::
   err1: TypeForm[str | None] = str | int  # Error
   err2: TypeForm[str | None] = list[str | None]  # Error
 
-By this same definition, ``TypeForm[Any]`` describes a type form object
-that represents the type ``Any`` or any type that is assignable to ``Any``.
-Since all types in the Python type system are assignable to ``Any``,
-``TypeForm[Any]`` describes the set of all type form objects
-evaluated from all valid type expressions.
+By this same definition, ``TypeForm[object]`` describes a type form object that
+represents the type ``object`` or any type that is assignable to ``object``.
+Since all types in the Python type system are assignable to ``object``,
+``TypeForm[object]`` describes the set of all type form objects evaluated from
+all valid type expressions.
+
+``TypeForm[Any]`` describes a ``TypeForm`` type whose type argument is not
+statically known, and is thus assignable both to and from any other
+``TypeForm`` type (because ``Any`` is assignable both to and from any type.)
 
 The type expression ``TypeForm``, with no type argument provided, is
 equivalent to ``TypeForm[Any]``.
@@ -289,9 +293,9 @@ This explicit syntax serves two purposes. First, it documents the developer's
 intent to use the value as a type form object. Second, static type checkers
 validate that all rules for type expressions are followed::
 
-  x4 = type(int)  # No error, evaluates to "type[int]"
+  x4 = type(1)  # No error, evaluates to "type[int]"
   
-  x5 = TypeForm(type(int))  # Error: call not allowed in type expression
+  x5 = TypeForm(type(1))  # Error: call not allowed in type expression
 
 
 Assignability
@@ -533,21 +537,26 @@ of ``type``.
 Treat ``type[T]`` as a subtype of ``TypeForm[T]``
 -------------------------------------------------
 
-It was suggested that type ``type[T]`` should be considered a subtype
-of ``TypeForm[T]``. This was ultimately rejected because there are ways to
-create an object of type ``type[T]`` that does not encode a valid type expression.
-For example, the expression ``type[1]`` is not a valid type expression. Likewise,
-the  expression ``type[S]`` is not a valid type expression if ``S`` is an
-out-of-scope type variable. This same argument applies to other special forms
-like objects of type ``UnionType``, which may or may not encode a valid type
-expression. Rather than carving out a special case for ``type[T]`` that would
-allow for potential unsoundness, it was decided to treat all type forms
-consistently. Therefore, ``type[T]`` is not considered a subtype of ``TypeForm[T]``.
-
-It was also pointed out that the expression ``C | C`` (where ``C`` is a class
-object) is a valid type expression - and therefore a valid ``TypeForm``,
-but its runtime type form encoding is an instance of ``UnionType`` and
-therefore is not compatible with ``type[C]``.
+It was suggested that type ``type[T]`` should be considered a subtype of
+``TypeForm[T]``. This is intuitive because, given a class ``C``, the expression
+``C`` both evaluates at runtime to the type object ``C`` (which inhabits the
+type ``type[C]``), and is also a valid type expression spelling the type ``C``
+(therefore also inhabits the type ``TypeForm[C]``).
+
+The problem is that there are other expressions (for example,
+``C().__class__``), which also evaluate to the class object ``C``, but are not
+valid type expressions spelling the type ``C``, therefore should not inhabit
+``TypeForm[C]``. In order to maintain consistency that ``TypeForm`` types may
+only originate in valid type expressions, we say that ``type[T]`` is not a
+subtype of ``TypeForm[T]``. (This implies that the type system considers the
+objects resulting from ``C`` and ``C().__class__`` to be distinguishable, in
+that the former is a valid ``TypeForm`` and the latter is not, even though they
+are identical at runtime.)
+
+``TypeForm[T]`` is also not a subtype of ``type[T]``, because the expression
+``C | C`` (where ``C`` is a class object) is a valid type expression - and
+therefore a valid ``TypeForm``, but its runtime type form encoding is an
+instance of ``UnionType`` and therefore does not inhabit ``type[C]``.
 
 If a function wishes to indicate that it accepts values of type ``TypeForm[T]``
 _and_ ``type[T]``, the parameter can simply be annotated with a union of these