diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/README.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/README.md
new file mode 100644
index 0000000000..99fa88d552
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/README.md
@@ -0,0 +1,20 @@
+# Type compendium
+
+The type compendium contains "fact sheets" about important, interesting, and peculiar types in (ty's
+interpretation of) Python's type system. It is meant to be an educational reference for developers
+and users of ty. It is also a living document that ensures that our implementation of these types
+and their properties is consistent with the specification.
+
+## Table of contents
+
+- [`Never`](never.md)
+- [`Object`](object.md)
+- [`None`](none.md)
+- [Integer `Literal`s](integer_literals.md)
+- String `Literal`s, `LiteralString`
+- [`tuple` types](tuple.md)
+- Class instance types
+- [`Any`](any.md)
+- Class literal types, `type[C]`, `type[object]`, `type[Any]`
+- [`AlwaysTruthy`, `AlwaysFalsy`](always_truthy_falsy.md)
+- [`Not[T]`](not_t.md)
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/always_truthy_falsy.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/always_truthy_falsy.md
new file mode 100644
index 0000000000..ede8b40a30
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/always_truthy_falsy.md
@@ -0,0 +1,175 @@
+# `AlwaysTruthy` and `AlwaysFalsy`
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+The types `AlwaysTruthy` and `AlwaysFalsy` describe the set of values that are always truthy or
+always falsy, respectively. More concretely, a value `at` is of type `AlwaysTruthy` if we can
+statically infer that `bool(at)` is always `True`, i.e. that the expression `bool(at)` has type
+`Literal[True]`. Conversely, a value `af` is of type `AlwaysFalsy` if we can statically infer that
+`bool(af)` is always `False`, i.e. that `bool(af)` has type `Literal[False]`.
+
+## Examples
+
+Here, we give a few examples of values that belong to these types:
+
+```py
+from ty_extensions import AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Literal
+
+class CustomAlwaysTruthyType:
+    def __bool__(self) -> Literal[True]:
+        return True
+
+class CustomAlwaysFalsyType:
+    def __bool__(self) -> Literal[False]:
+        return False
+
+at: AlwaysTruthy
+at = True
+at = 1
+at = 123
+at = -1
+at = "non empty"
+at = b"non empty"
+at = CustomAlwaysTruthyType()
+
+af: AlwaysFalsy
+af = False
+af = None
+af = 0
+af = ""
+af = b""
+af = CustomAlwaysFalsyType()
+```
+
+## `AlwaysTruthy` and `AlwaysFalsy` are disjoint
+
+It follows directly from the definition that `AlwaysTruthy` and `AlwaysFalsy` are disjoint types:
+
+```py
+from ty_extensions import static_assert, is_disjoint_from, AlwaysTruthy, AlwaysFalsy
+
+static_assert(is_disjoint_from(AlwaysTruthy, AlwaysFalsy))
+```
+
+## `Truthy` and `Falsy`
+
+It is useful to also define the types `Truthy = ~AlwaysFalsy` and `Falsy = ~AlwaysTruthy`. These
+types describe the set of values that *can* be truthy (`bool(t)` can return `True`) or falsy
+(`bool(f)` can return `False`), respectively.
+
+Finally, we can also define the type `AmbiguousTruthiness = Truthy & Falsy`, which describes the set
+of values that can be truthy *and* falsy. This intersection is not empty. In the following, we give
+examples for values that belong to these three types:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to, is_disjoint_from, Not, Intersection, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Never
+from random import choice
+
+type Truthy = Not[AlwaysFalsy]
+type Falsy = Not[AlwaysTruthy]
+
+type AmbiguousTruthiness = Intersection[Truthy, Falsy]
+
+static_assert(is_disjoint_from(AlwaysTruthy, AmbiguousTruthiness))
+static_assert(is_disjoint_from(AlwaysFalsy, AmbiguousTruthiness))
+static_assert(not is_disjoint_from(Truthy, Falsy))
+
+class CustomAmbiguousTruthinessType:
+    def __bool__(self) -> bool:
+        return choice((True, False))
+
+def maybe_empty_list() -> list[int]:
+    return choice(([], [1, 2, 3]))
+
+reveal_type(bool(maybe_empty_list()))  # revealed: bool
+reveal_type(bool(CustomAmbiguousTruthinessType()))  # revealed: bool
+
+t: Truthy
+t = True
+t = 1
+# TODO: This assignment should be okay
+t = maybe_empty_list()  # error: [invalid-assignment]
+# TODO: This assignment should be okay
+t = CustomAmbiguousTruthinessType()  # error: [invalid-assignment]
+
+a: AmbiguousTruthiness
+# TODO: This assignment should be okay
+a = maybe_empty_list()  # error: [invalid-assignment]
+# TODO: This assignment should be okay
+a = CustomAmbiguousTruthinessType()  # error: [invalid-assignment]
+
+f: Falsy
+f = False
+f = None
+# TODO: This assignment should be okay
+f = maybe_empty_list()  # error: [invalid-assignment]
+# TODO: This assignment should be okay
+f = CustomAmbiguousTruthinessType()  # error: [invalid-assignment]
+```
+
+## Subtypes of `AlwaysTruthy`, `AlwaysFalsy`
+
+```py
+from ty_extensions import static_assert, is_subtype_of, is_disjoint_from, AlwaysTruthy, AlwaysFalsy
+from typing_extensions import Literal
+```
+
+These two types are disjoint, so types (that are not equivalent to Never) can only be a subtype of
+either one of them.
+
+```py
+static_assert(is_disjoint_from(AlwaysTruthy, AlwaysFalsy))
+```
+
+Types that only contain always-truthy values
+
+```py
+static_assert(is_subtype_of(Literal[True], AlwaysTruthy))
+static_assert(is_subtype_of(Literal[1], AlwaysTruthy))
+static_assert(is_subtype_of(Literal[-1], AlwaysTruthy))
+static_assert(is_subtype_of(Literal["non empty"], AlwaysTruthy))
+static_assert(is_subtype_of(Literal[b"non empty"], AlwaysTruthy))
+```
+
+Types that only contain always-falsy values
+
+```py
+static_assert(is_subtype_of(None, AlwaysFalsy))
+static_assert(is_subtype_of(Literal[False], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[0], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[""], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[b""], AlwaysFalsy))
+static_assert(is_subtype_of(Literal[False] | Literal[0], AlwaysFalsy))
+```
+
+Ambiguous truthiness types
+
+```py
+static_assert(not is_subtype_of(bool, AlwaysTruthy))
+static_assert(not is_subtype_of(bool, AlwaysFalsy))
+
+static_assert(not is_subtype_of(list[int], AlwaysTruthy))
+static_assert(not is_subtype_of(list[int], AlwaysFalsy))
+```
+
+## Open questions
+
+Is `tuple[()]` always falsy? We currently model it this way, but this is
+[under discussion](https://github.com/astral-sh/ruff/issues/15528).
+
+```py
+from ty_extensions import static_assert, is_subtype_of, AlwaysFalsy
+
+static_assert(is_subtype_of(tuple[()], AlwaysFalsy))
+```
+
+## References
+
+See also:
+
+- Our test suite on [narrowing for `if x` and `if not x`](../narrow/truthiness.md).
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/any.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/any.md
new file mode 100644
index 0000000000..da545f70a2
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/any.md
@@ -0,0 +1,141 @@
+# `Any`
+
+## Introduction
+
+The type `Any` is the dynamic type in Python's gradual type system. It represents an unknown
+fully-static type, which means that it represents an *unknown* set of runtime values.
+
+```py
+from ty_extensions import static_assert, is_fully_static
+from typing import Any
+```
+
+`Any` is a dynamic type:
+
+```py
+static_assert(not is_fully_static(Any))
+```
+
+## Every type is assignable to `Any`, and `Any` is assignable to every type
+
+```py
+from ty_extensions import static_assert, is_fully_static, is_assignable_to
+from typing_extensions import Never, Any
+
+class C: ...
+
+static_assert(is_assignable_to(C, Any))
+static_assert(is_assignable_to(Any, C))
+
+static_assert(is_assignable_to(object, Any))
+static_assert(is_assignable_to(Any, object))
+
+static_assert(is_assignable_to(Never, Any))
+static_assert(is_assignable_to(Any, Never))
+
+static_assert(is_assignable_to(type, Any))
+static_assert(is_assignable_to(Any, type))
+
+static_assert(is_assignable_to(type[Any], Any))
+static_assert(is_assignable_to(Any, type[Any]))
+```
+
+`Any` is also assignable to itself (like every type):
+
+```py
+static_assert(is_assignable_to(Any, Any))
+```
+
+## Unions with `Any`: `Any | T`
+
+The union `Any | T` of `Any` with a fully static type `T` describes an unknown set of values that is
+*at least as large* as the set of values described by `T`. It represents an unknown fully-static
+type with *lower bound* `T`. Again, this can be demonstrated using the assignable-to relation:
+
+```py
+from ty_extensions import static_assert, is_assignable_to, is_equivalent_to
+from typing_extensions import Any
+
+# A class hierarchy Small <: Medium <: Big
+
+class Big: ...
+class Medium(Big): ...
+class Small(Medium): ...
+
+static_assert(is_assignable_to(Any | Medium, Big))
+static_assert(is_assignable_to(Any | Medium, Medium))
+
+# `Any | Medium` is at least as large as `Medium`, so we can not assign it to `Small`:
+static_assert(not is_assignable_to(Any | Medium, Small))
+```
+
+The union `Any | object` is equivalent to `object`. This is true for every union with `object`, but
+it is worth demonstrating:
+
+```py
+static_assert(is_equivalent_to(Any | object, object))
+static_assert(is_equivalent_to(object | Any, object))
+```
+
+## Intersections with `Any`: `Any & T`
+
+The intersection `Any & T` of `Any` with a fully static type `T` describes an unknown set of values
+that is *no larger than* the set of values described by `T`. It represents an unknown fully-static
+type with *upper bound* `T`:
+
+```py
+from ty_extensions import static_assert, is_assignable_to, Intersection, is_equivalent_to
+from typing import Any
+
+class Big: ...
+class Medium(Big): ...
+class Small(Medium): ...
+
+static_assert(is_assignable_to(Small, Intersection[Any, Medium]))
+static_assert(is_assignable_to(Medium, Intersection[Any, Medium]))
+```
+
+`Any & Medium` is no larger than `Medium`, so we can not assign `Big` to it. There is no possible
+materialization of `Any & Medium` that would make it as big as `Big`:
+
+```py
+static_assert(not is_assignable_to(Big, Intersection[Any, Medium]))
+```
+
+`Any & Never` represents an "unknown" fully-static type which is no larger than `Never`. There is no
+such fully-static type, except for `Never` itself. So `Any & Never` is equivalent to `Never`:
+
+```py
+from typing_extensions import Never
+
+static_assert(is_equivalent_to(Intersection[Any, Never], Never))
+static_assert(is_equivalent_to(Intersection[Never, Any], Never))
+```
+
+## Tuples with `Any`
+
+This section demonstrates the following passage from the [type system concepts] documentation on
+gradual types:
+
+> A type such as `tuple[int, Any]` […] does not represent a single set of Python objects; rather, it
+> represents a (bounded) range of possible sets of values. […] In the same way that `Any` does not
+> represent "the set of all Python objects" but rather "an unknown set of objects",
+> `tuple[int, Any]` does not represent "the set of all length-two tuples whose first element is an
+> integer". That is a fully static type, spelled `tuple[int, object]`. By contrast,
+> `tuple[int, Any]` represents some unknown set of tuple values; it might be the set of all tuples
+> of two integers, or the set of all tuples of an integer and a string, or some other set of tuple
+> values.
+>
+> In practice, this difference is seen (for example) in the fact that we can assign an expression of
+> type `tuple[int, Any]` to a target typed as `tuple[int, int]`, whereas assigning
+> `tuple[int, object]` to `tuple[int, int]` is a static type error.
+
+```py
+from ty_extensions import static_assert, is_assignable_to
+from typing import Any
+
+static_assert(is_assignable_to(tuple[int, Any], tuple[int, int]))
+static_assert(not is_assignable_to(tuple[int, object], tuple[int, int]))
+```
+
+[type system concepts]: https://typing.readthedocs.io/en/latest/spec/concepts.html#gradual-types
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/integer_literals.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/integer_literals.md
new file mode 100644
index 0000000000..d8d42ae7ad
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/integer_literals.md
@@ -0,0 +1,234 @@
+# Integer `Literal`s
+
+An integer literal type represents the set of all integer objects with one specific value. For
+example, the type `Literal[54165]` represents the set of all integer objects with the value `54165`.
+
+## Integer `Literal`s are not singleton types
+
+This does not necessarily mean that the type is a singleton type, i.e., a type with only one
+inhabitant. The reason for this is that there might be multiple Python runtime objects (at different
+memory locations) that all represent the same integer value. For example, the following code snippet
+may print `False`.
+
+```py
+x = 54165
+y = 54165
+
+print(x is y)
+```
+
+In practice, on CPython 3.13.0, this program prints `True` when executed as a script, but `False`
+when executed in the REPL.
+
+Since this is an implementation detail of the Python runtime, we model all integer literals as
+non-singleton types:
+
+```py
+from ty_extensions import static_assert, is_singleton
+from typing import Literal
+
+static_assert(not is_singleton(Literal[0]))
+static_assert(not is_singleton(Literal[1]))
+static_assert(not is_singleton(Literal[54165]))
+```
+
+This has implications for type-narrowing. For example, you can not use the `is not` operator to
+check whether a variable has a specific integer literal type, but this is not a recommended practice
+anyway.
+
+```py
+def f(x: int):
+    if x is 54165:
+        # This works, because if `x` is the same object as that left-hand-side literal, then it
+        # must have the same value.
+        reveal_type(x)  # revealed: Literal[54165]
+
+    if x is not 54165:
+        # But here, we can not narrow the type (to `int & ~Literal[54165]`), because `x` might also
+        # have the value `54165`, but a different object identity.
+        reveal_type(x)  # revealed: int
+```
+
+## Integer `Literal`s are single-valued types
+
+There is a slightly weaker property that integer literals have. They are single-valued types, which
+means that all objects of the type have the same value, i.e. they compare equal to each other:
+
+```py
+from ty_extensions import static_assert, is_single_valued
+from typing import Literal
+
+static_assert(is_single_valued(Literal[0]))
+static_assert(is_single_valued(Literal[1]))
+static_assert(is_single_valued(Literal[54165]))
+```
+
+And this can be used for type-narrowing using not-equal comparisons:
+
+```py
+def f(x: int):
+    if x == 54165:
+        # The reason that no narrowing occurs here is that there might be subclasses of `int`
+        # that override `__eq__`. This is not specific to integer literals though, and generally
+        # applies to `==` comparisons.
+        reveal_type(x)  # revealed: int
+
+    if x != 54165:
+        reveal_type(x)  # revealed: int & ~Literal[54165]
+```
+
+## Subtyping relationships
+
+### Subtypes of `int`
+
+All integer literals are subtypes of `int`:
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+from typing import Literal
+
+static_assert(is_subtype_of(Literal[0], int))
+static_assert(is_subtype_of(Literal[1], int))
+static_assert(is_subtype_of(Literal[54165], int))
+```
+
+It is tempting to think that `int` is equivalent to the union of all integer literals,
+`… | Literal[-1] | Literal[0] | Literal[1] | …`, but this is not the case. `True` and `False` are
+also inhabitants of the `int` type, but they are not inhabitants of any integer literal type:
+
+```py
+static_assert(is_subtype_of(Literal[True], int))
+static_assert(is_subtype_of(Literal[False], int))
+
+static_assert(not is_subtype_of(Literal[True], Literal[1]))
+static_assert(not is_subtype_of(Literal[False], Literal[0]))
+```
+
+Also, `int` can be subclassed, and instances of that subclass are also subtypes of `int`:
+
+```py
+class CustomInt(int):
+    pass
+
+static_assert(is_subtype_of(CustomInt, int))
+```
+
+### No subtypes of `float` and `complex`
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+Integer literals are _not_ subtypes of `float`, but the typing spec describes a special case for
+[`float` and `complex`] which accepts integers (and therefore also integer literals) in places where
+a `float` or `complex` is expected. We use the types `JustFloat` and `JustComplex` below, because ty
+recognizes an annotation of `float` as `int | float` to support that typing system special case.
+
+```py
+from ty_extensions import static_assert, is_subtype_of, JustFloat, JustComplex
+from typing import Literal
+
+# Not subtypes of `float` and `complex`
+static_assert(not is_subtype_of(Literal[0], JustFloat) and not is_subtype_of(Literal[0], JustComplex))
+static_assert(not is_subtype_of(Literal[1], JustFloat) and not is_subtype_of(Literal[1], JustComplex))
+static_assert(not is_subtype_of(Literal[54165], JustFloat) and not is_subtype_of(Literal[54165], JustComplex))
+```
+
+The typing system special case can be seen in the following example:
+
+```py
+a: JustFloat = 1  # error: [invalid-assignment]
+b: JustComplex = 1  # error: [invalid-assignment]
+
+x: float = 1
+y: complex = 1
+```
+
+### Subtypes of integer `Literal`s?
+
+The only subtypes of an integer literal type _that can be named_ are the type itself and `Never`:
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+from typing_extensions import Never, Literal
+
+static_assert(is_subtype_of(Literal[54165], Literal[54165]))
+static_assert(is_subtype_of(Never, Literal[54165]))
+```
+
+## Disjointness of integer `Literal`s
+
+Two integer literal types `Literal[a]` and `Literal[b]` are disjoint if `a != b`:
+
+```py
+from ty_extensions import static_assert, is_disjoint_from
+from typing import Literal
+
+static_assert(is_disjoint_from(Literal[0], Literal[1]))
+static_assert(is_disjoint_from(Literal[0], Literal[54165]))
+
+static_assert(not is_disjoint_from(Literal[0], Literal[0]))
+static_assert(not is_disjoint_from(Literal[54165], Literal[54165]))
+```
+
+## Integer literal math
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+We support a whole range of arithmetic operations on integer literal types. For example, we can
+statically verify that (3, 4, 5) is a Pythagorean triple:
+
+```py
+from ty_extensions import static_assert
+
+static_assert(3**2 + 4**2 == 5**2)
+```
+
+Using unions of integer literals, we can even use this to solve equations over a finite domain
+(determine whether there is a solution or not):
+
+```py
+from typing import Literal, assert_type
+
+type Nat = Literal[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
+
+def pythagorean_triples(a: Nat, b: Nat, c: Nat):
+    # Answer is `bool`, because solutions do exist (3² + 4² = 5²)
+    assert_type(a**2 + b**2 == c**2, bool)
+
+def fermats_last_theorem(a: Nat, b: Nat, c: Nat):
+    # Answer is `Literal[False]`, because no solutions exist
+    assert_type(a**3 + b**3 == c**3, Literal[False])
+```
+
+## Truthiness
+
+Integer literals are always-truthy, except for `0`, which is always-falsy:
+
+```py
+from ty_extensions import static_assert
+
+static_assert(-54165)
+static_assert(-1)
+static_assert(not 0)
+static_assert(1)
+static_assert(54165)
+```
+
+This can be used for type-narrowing:
+
+```py
+from typing_extensions import Literal, assert_type
+
+def f(x: Literal[0, 1, 54365]):
+    if x:
+        assert_type(x, Literal[1, 54365])
+    else:
+        assert_type(x, Literal[0])
+```
+
+[`float` and `complex`]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/never.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/never.md
new file mode 100644
index 0000000000..98bff577a2
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/never.md
@@ -0,0 +1,185 @@
+# `Never`
+
+`Never` represents the empty set of values.
+
+## `Never` is a subtype of every type
+
+The `Never` type is the bottom type of Python's type system. It is a subtype of every type, but no
+type is a subtype of `Never`, except for `Never` itself.
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+from typing_extensions import Never
+
+class C: ...
+
+static_assert(is_subtype_of(Never, int))
+static_assert(is_subtype_of(Never, object))
+static_assert(is_subtype_of(Never, C))
+static_assert(is_subtype_of(Never, Never))
+
+static_assert(not is_subtype_of(int, Never))
+```
+
+## `Never` is assignable to every type
+
+`Never` is assignable to every type. This fact is useful when calling error-handling functions in a
+context that requires a value of a specific type. For example, changing the `Never` return type to
+`None` below would cause a type error:
+
+```py
+from ty_extensions import static_assert, is_assignable_to
+from typing_extensions import Never, Any
+
+static_assert(is_assignable_to(Never, int))
+static_assert(is_assignable_to(Never, object))
+static_assert(is_assignable_to(Never, Any))
+static_assert(is_assignable_to(Never, Never))
+
+def raise_error() -> Never:
+    raise Exception("...")
+
+def f(divisor: int) -> None:
+    x: float = (1 / divisor) if divisor != 0 else raise_error()
+```
+
+## `Never` in annotations
+
+`Never` can be used in functions to indicate that the function never returns. For example, if a
+function always raises an exception, if it calls `sys.exit()`, if it enters an infinite loop, or if
+it calls itself recursively. All of these functions "Never" return control back to the caller:
+
+```py
+from typing_extensions import Never
+
+def raises_unconditionally() -> Never:
+    raise Exception("This function always raises an exception")
+
+def exits_unconditionally() -> Never:
+    import sys
+
+    return sys.exit(1)
+
+def loops_forever() -> Never:
+    while True:
+        pass
+
+def recursive_never() -> Never:
+    return recursive_never()
+```
+
+Similarly, if `Never` is used in parameter positions, it indicates that the function can "Never" be
+called, because it can never be passed a value of type `Never` (there are none):
+
+```py
+def can_not_be_called(n: Never) -> int:
+    return 0
+```
+
+## `Never` is disjoint from every other type
+
+Two types `A` and `B` are disjoint if their intersection is empty. Since `Never` has no inhabitants,
+it is disjoint from every other type:
+
+```py
+from ty_extensions import static_assert, is_disjoint_from
+from typing_extensions import Never
+
+class C: ...
+
+static_assert(is_disjoint_from(Never, int))
+static_assert(is_disjoint_from(Never, object))
+static_assert(is_disjoint_from(Never, C))
+static_assert(is_disjoint_from(Never, Never))
+```
+
+## Unions with `Never`
+
+`Never` can always be removed from unions:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+from typing_extensions import Never
+
+class P: ...
+class Q: ...
+
+static_assert(is_equivalent_to(P | Never | Q | None, P | Q | None))
+```
+
+## Intersections with `Never`
+
+Intersecting with `Never` results in `Never`:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to, Intersection
+from typing_extensions import Never
+
+class P: ...
+class Q: ...
+
+static_assert(is_equivalent_to(Intersection[P, Never, Q], Never))
+```
+
+## `Never` is the complement of `object`
+
+`object` describes the set of all possible values, while `Never` describes the empty set. The two
+types are complements of each other:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to, Not
+from typing_extensions import Never
+
+static_assert(is_equivalent_to(Not[object], Never))
+static_assert(is_equivalent_to(Not[Never], object))
+```
+
+This duality is also reflected in other facts:
+
+- `Never` is a subtype of every type, while `object` is a supertype of every type.
+- `Never` is assignable to every type, while `object` is assignable from every type.
+- `Never` is disjoint from every type, while `object` overlaps with every type.
+- Building a union with `Never` is a no-op, intersecting with `object` is a no-op.
+- Interecting with `Never` results in `Never`, building a union with `object` results in `object`.
+
+## Lists of `Never`
+
+`list[Never]` is a reasonable type that is *not* equivalent to `Never`. The empty list inhabits this
+type:
+
+```py
+from typing_extensions import Never
+
+x: list[Never] = []
+```
+
+## Tuples involving `Never`
+
+A type like `tuple[int, Never]` has no inhabitants, and so it is equivalent to `Never`:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+from typing_extensions import Never
+
+static_assert(is_equivalent_to(tuple[int, Never], Never))
+```
+
+Note that this is not the case for the homogenous tuple type `tuple[Never, ...]` though, because
+that type is inhabited by the empty tuple:
+
+```py
+static_assert(not is_equivalent_to(tuple[Never, ...], Never))
+
+t: tuple[Never, ...] = ()
+```
+
+## `NoReturn` is the same as `Never`
+
+The `NoReturn` type is a different name for `Never`:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+from typing_extensions import NoReturn, Never
+
+static_assert(is_equivalent_to(NoReturn, Never))
+```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/none.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/none.md
new file mode 100644
index 0000000000..08fcd7905b
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/none.md
@@ -0,0 +1,80 @@
+# `None`
+
+## `None` as a singleton type
+
+The type `None` (or `NoneType`, see below) is a singleton type that has only one inhabitant: the
+object `None`.
+
+```py
+from ty_extensions import static_assert, is_singleton, is_equivalent_to
+
+n: None = None
+
+static_assert(is_singleton(None))
+```
+
+Just like for other singleton types, the only subtypes of `None` are `None` itself and `Never`:
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+from typing_extensions import Never
+
+static_assert(is_subtype_of(None, None))
+static_assert(is_subtype_of(Never, None))
+```
+
+## Relationship to `Optional[T]`
+
+The type `Optional[T]` is an alias for `T | None` (or `Union[T, None]`):
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+from typing import Optional, Union
+
+class T: ...
+
+static_assert(is_equivalent_to(Optional[T], T | None))
+static_assert(is_equivalent_to(Optional[T], Union[T, None]))
+```
+
+## Type narrowing using `is`
+
+Just like for other singleton types, we support type narrowing using `is` or `is not` checks:
+
+```py
+from typing_extensions import assert_type
+
+class T: ...
+
+def f(x: T | None):
+    if x is None:
+        assert_type(x, None)
+    else:
+        assert_type(x, T)
+
+    assert_type(x, T | None)
+
+    if x is not None:
+        assert_type(x, T)
+    else:
+        assert_type(x, None)
+```
+
+## `NoneType`
+
+`None` is special in that the name of the instance at runtime can be used as a type as well: The
+object `None` is an instance of type `None`. When a distinction between the two is needed, the
+spelling `NoneType` can be used, which is available since Python 3.10. `NoneType` is equivalent to
+`None`:
+
+```toml
+[environment]
+python-version = "3.10"
+```
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+from types import NoneType
+
+static_assert(is_equivalent_to(NoneType, None))
+```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/not_t.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/not_t.md
new file mode 100644
index 0000000000..962e30f507
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/not_t.md
@@ -0,0 +1,120 @@
+# `Not[T]`
+
+The type `Not[T]` is the complement of the type `T`. It describes the set of all values that are
+*not* in `T`.
+
+## `Not[T]` is disjoint from `T`
+
+`Not[T]` is disjoint from `T`:
+
+```py
+from ty_extensions import Not, static_assert, is_disjoint_from
+
+class T: ...
+class S(T): ...
+
+static_assert(is_disjoint_from(Not[T], T))
+static_assert(is_disjoint_from(Not[T], S))
+```
+
+## The union of `T` and `Not[T]` is equivalent to `object`
+
+Together, `T` and `Not[T]` describe the set of all values. So the union of both types is equivalent
+to `object`:
+
+```py
+from ty_extensions import Not, static_assert, is_equivalent_to
+
+class T: ...
+
+static_assert(is_equivalent_to(T | Not[T], object))
+```
+
+## `Not[T]` reverses subtyping relationships
+
+If `S <: T`, then `Not[T] <: Not[S]`:, similar to how negation in logic reverses the order of `<=`:
+
+```py
+from ty_extensions import Not, static_assert, is_subtype_of
+
+class T: ...
+class S(T): ...
+
+static_assert(is_subtype_of(S, T))
+static_assert(is_subtype_of(Not[T], Not[S]))
+```
+
+## `Not[T]` reverses assignability relationships
+
+Assignability relationships are similarly reversed:
+
+```py
+from ty_extensions import Not, Intersection, static_assert, is_assignable_to
+from typing import Any
+
+class T: ...
+class S(T): ...
+
+static_assert(is_assignable_to(S, T))
+static_assert(is_assignable_to(Not[T], Not[S]))
+
+static_assert(is_assignable_to(Intersection[Any, S], Intersection[Any, T]))
+
+static_assert(is_assignable_to(Not[Intersection[Any, S]], Not[Intersection[Any, T]]))
+```
+
+## Subtyping and disjointness
+
+If two types `P` and `Q` are disjoint, then `P` must be a subtype of `Not[Q]`, and vice versa:
+
+```py
+from ty_extensions import Not, static_assert, is_subtype_of, is_disjoint_from
+from typing import final
+
+@final
+class P: ...
+
+@final
+class Q: ...
+
+static_assert(is_disjoint_from(P, Q))
+
+static_assert(is_subtype_of(P, Not[Q]))
+static_assert(is_subtype_of(Q, Not[P]))
+```
+
+## De-Morgan's laws
+
+Given two unrelated types `P` and `Q`, we can demonstrate De-Morgan's laws in the context of
+set-theoretic types:
+
+```py
+from ty_extensions import Not, static_assert, is_equivalent_to, Intersection
+
+class P: ...
+class Q: ...
+```
+
+The negation of a union is the intersection of the negations:
+
+```py
+static_assert(is_equivalent_to(Not[P | Q], Intersection[Not[P], Not[Q]]))
+```
+
+Conversely, the negation of an intersection is the union of the negations:
+
+```py
+static_assert(is_equivalent_to(Not[Intersection[P, Q]], Not[P] | Not[Q]))
+```
+
+## Negation of gradual types
+
+`Any` represents an unknown set of values. So `Not[Any]` also represents an unknown set of values.
+The two gradual types are equivalent:
+
+```py
+from ty_extensions import static_assert, is_gradual_equivalent_to, Not
+from typing import Any
+
+static_assert(is_gradual_equivalent_to(Not[Any], Any))
+```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/object.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/object.md
new file mode 100644
index 0000000000..f8c9e4fec2
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/object.md
@@ -0,0 +1,78 @@
+# `object`
+
+The `object` type represents the set of all Python objects.
+
+## `object` is a supertype of all types
+
+It is the top type in Python's type system, i.e., it is a supertype of all other types:
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+
+static_assert(is_subtype_of(int, object))
+static_assert(is_subtype_of(str, object))
+static_assert(is_subtype_of(type, object))
+static_assert(is_subtype_of(object, object))
+```
+
+## Every type is assignable to `object`
+
+Everything can be assigned to the type `object`. This fact can be used to create heterogeneous
+collections of objects (but also erases more specific type information):
+
+```py
+from ty_extensions import static_assert, is_assignable_to
+from typing_extensions import Any, Never
+
+static_assert(is_assignable_to(int, object))
+static_assert(is_assignable_to(str | bytes, object))
+static_assert(is_assignable_to(type, object))
+static_assert(is_assignable_to(object, object))
+static_assert(is_assignable_to(Never, object))
+static_assert(is_assignable_to(Any, object))
+
+x: list[object] = [1, "a", ()]
+```
+
+## `object` overlaps with all types
+
+There is no type that is disjoint from `object` except for `Never`:
+
+```py
+from ty_extensions import static_assert, is_disjoint_from
+from typing_extensions import Any, Never
+
+static_assert(not is_disjoint_from(int, object))
+static_assert(not is_disjoint_from(str, object))
+static_assert(not is_disjoint_from(type, object))
+static_assert(not is_disjoint_from(object, object))
+static_assert(not is_disjoint_from(Any, object))
+static_assert(is_disjoint_from(Never, object))
+```
+
+## Unions with `object`
+
+Unions with `object` are equivalent to `object`:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to
+
+static_assert(is_equivalent_to(int | object | None, object))
+```
+
+## Intersections with `object`
+
+Intersecting with `object` is equivalent to the original type:
+
+```py
+from ty_extensions import static_assert, is_equivalent_to, Intersection
+
+class P: ...
+class Q: ...
+
+static_assert(is_equivalent_to(Intersection[P, object, Q], Intersection[P, Q]))
+```
+
+## `object` is the complement of `Never`
+
+See corresponding section in the fact sheet for [`Never`](never.md).
diff --git a/crates/ty_python_semantic/resources/mdtest/type_compendium/tuple.md b/crates/ty_python_semantic/resources/mdtest/type_compendium/tuple.md
new file mode 100644
index 0000000000..350ee0123e
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_compendium/tuple.md
@@ -0,0 +1,166 @@
+# Tuples
+
+## Tuples as product types
+
+Tuples can be used to construct product types. Inhabitants of the type `tuple[P, Q]` are ordered
+pairs `(p, q)` where `p` is an inhabitant of `P` and `q` is an inhabitant of `Q`, analogous to the
+Cartesian product of sets.
+
+```py
+from typing_extensions import assert_type
+
+class P: ...
+class Q: ...
+
+def _(p: P, q: Q):
+    assert_type((p, q), tuple[P, Q])
+```
+
+## Subtyping relationships
+
+The type `tuple[S1, S2]` is a subtype of `tuple[T1, T2]` if and only if `S1` is a subtype of `T1`
+and `S2` is a subtype of `T2`, and similar for other lengths of tuples:
+
+```py
+from ty_extensions import static_assert, is_subtype_of
+
+class T1: ...
+class S1(T1): ...
+class T2: ...
+class S2(T2): ...
+
+static_assert(is_subtype_of(tuple[S1], tuple[T1]))
+static_assert(not is_subtype_of(tuple[T1], tuple[S1]))
+
+static_assert(is_subtype_of(tuple[S1, S2], tuple[T1, T2]))
+static_assert(not is_subtype_of(tuple[T1, S2], tuple[S1, T2]))
+static_assert(not is_subtype_of(tuple[S1, T2], tuple[T1, S2]))
+```
+
+Different-length tuples are not related via subtyping:
+
+```py
+static_assert(not is_subtype_of(tuple[S1], tuple[T1, T2]))
+```
+
+## The empty tuple
+
+The type of the empty tuple `()` is spelled `tuple[()]`. It is [not a singleton type], because
+different instances of `()` are not guaranteed to be the same object (even if this is the case in
+CPython at the time of writing).
+
+The empty tuple can also be subclassed (further clarifying that it is not a singleton type):
+
+```py
+from ty_extensions import static_assert, is_singleton, is_subtype_of, is_equivalent_to, is_assignable_to
+
+static_assert(not is_singleton(tuple[()]))
+
+class AnotherEmptyTuple(tuple[()]): ...
+
+static_assert(not is_equivalent_to(AnotherEmptyTuple, tuple[()]))
+
+# TODO: These should not be errors
+# error: [static-assert-error]
+static_assert(is_subtype_of(AnotherEmptyTuple, tuple[()]))
+# error: [static-assert-error]
+static_assert(is_assignable_to(AnotherEmptyTuple, tuple[()]))
+```
+
+## Non-empty tuples
+
+For the same reason as above (two instances of a tuple with the same elements might not be the same
+object), non-empty tuples are also not singleton types — even if all their elements are singletons:
+
+```py
+from ty_extensions import static_assert, is_singleton
+
+static_assert(is_singleton(None))
+
+static_assert(not is_singleton(tuple[None]))
+```
+
+## Disjointness
+
+A tuple `tuple[P1, P2]` is disjoint from a tuple `tuple[Q1, Q2]` if either `P1` is disjoint from
+`Q1` or if `P2` is disjoint from `Q2`:
+
+```py
+from ty_extensions import static_assert, is_disjoint_from
+from typing import final
+
+@final
+class F1: ...
+
+@final
+class F2: ...
+
+class N1: ...
+class N2: ...
+
+static_assert(is_disjoint_from(F1, F2))
+static_assert(not is_disjoint_from(N1, N2))
+
+static_assert(is_disjoint_from(tuple[F1, F2], tuple[F2, F1]))
+static_assert(is_disjoint_from(tuple[F1, N1], tuple[F2, N2]))
+static_assert(is_disjoint_from(tuple[N1, F1], tuple[N2, F2]))
+static_assert(not is_disjoint_from(tuple[N1, N2], tuple[N2, N1]))
+```
+
+We currently model tuple types to *not* be disjoint from arbitrary instance types, because we allow
+for the possibility of `tuple` to be subclassed
+
+```py
+class C: ...
+
+static_assert(not is_disjoint_from(tuple[int, str], C))
+
+class CommonSubtype(tuple[int, str], C): ...
+```
+
+Note: This is inconsistent with the fact that we model heterogeneous tuples to be disjoint from
+other heterogeneous tuples above:
+
+```py
+class I1(tuple[F1, F2]): ...
+class I2(tuple[F2, F1]): ...
+
+# TODO
+# This is a subtype of both `tuple[F1, F2]` and `tuple[F2, F1]`, so those two heterogeneous tuples
+# should not be disjoint from each other (see conflicting test above).
+class CommonSubtypeOfTuples(I1, I2): ...
+```
+
+## Truthiness
+
+The truthiness of the empty tuple is `False`:
+
+```py
+from typing_extensions import assert_type, Literal
+
+assert_type(bool(()), Literal[False])
+```
+
+The truthiness of non-empty tuples is always `True`, even if all elements are falsy:
+
+```py
+from typing_extensions import assert_type, Literal
+
+assert_type(bool((False,)), Literal[True])
+assert_type(bool((False, False)), Literal[True])
+```
+
+Both of these results are conflicting with the fact that tuples can be subclassed, and that we
+currently allow subclasses of `tuple` to overwrite `__bool__` (or `__len__`):
+
+```py
+class NotAlwaysTruthyTuple(tuple[int]):
+    def __bool__(self) -> bool:
+        return False
+
+# TODO: This assignment should be allowed
+# error: [invalid-assignment]
+t: tuple[int] = NotAlwaysTruthyTuple((1,))
+```
+
+[not a singleton type]: https://discuss.python.org/t/should-we-specify-in-the-language-reference-that-the-empty-tuple-is-a-singleton/67957
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
index 8f0f360f09..b14e12f306 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
@@ -21,10 +21,7 @@ See the [typing documentation] for more information.
     as `int | float` and `int | float | complex`, respectively.
 
 ```py
-from ty_extensions import is_subtype_of, static_assert, TypeOf
-
-type JustFloat = TypeOf[1.0]
-type JustComplex = TypeOf[1j]
+from ty_extensions import is_subtype_of, static_assert, JustFloat, JustComplex
 
 static_assert(is_subtype_of(bool, bool))
 static_assert(is_subtype_of(bool, int))
@@ -88,9 +85,7 @@ static_assert(is_subtype_of(C, object))
 
 ```py
 from typing_extensions import Literal, LiteralString
-from ty_extensions import is_subtype_of, static_assert, TypeOf
-
-type JustFloat = TypeOf[1.0]
+from ty_extensions import is_subtype_of, static_assert, TypeOf, JustFloat
 
 # Boolean literals
 static_assert(is_subtype_of(Literal[True], bool))
diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi
index 0ed447e112..127f97c3c5 100644
--- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi
+++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi
@@ -14,6 +14,15 @@ Intersection: _SpecialForm
 TypeOf: _SpecialForm
 CallableTypeOf: _SpecialForm
 
+# ty treats annotations of `float` to mean `float | int`, and annotations of `complex`
+# to mean `complex | float | int`. This is to support a typing-system special case [1].
+# We therefore provide `JustFloat` and `JustComplex` to represent the "bare" `float` and
+# `complex` types, respectively.
+#
+# [1]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex
+type JustFloat = TypeOf[1.0]
+type JustComplex = TypeOf[1.0j]
+
 # Predicates on types
 #
 # Ideally, these would be annotated using `TypeForm`, but that has not been