diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 241178864..3f14c2642 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -84,8 +84,9 @@
 - [The HIR (High-level IR)](./hir.md)
     - [Lowering AST to HIR](./lowering.md)
     - [Debugging](./hir-debugging.md)
+- [The THIR (Typed High-level IR)](./thir.md)
 - [The MIR (Mid-level IR)](./mir/index.md)
-    - [THIR and MIR construction](./mir/construction.md)
+    - [MIR construction](./mir/construction.md)
     - [MIR visitor and traversal](./mir/visitor.md)
     - [MIR passes: getting the MIR for a function](./mir/passes.md)
 - [Identifiers in the Compiler](./identifiers.md)
diff --git a/src/mir/construction.md b/src/mir/construction.md
index d2c5a6f34..d9f99be03 100644
--- a/src/mir/construction.md
+++ b/src/mir/construction.md
@@ -1,4 +1,4 @@
-# THIR and MIR construction
+# MIR construction
 
 <!-- toc -->
 
@@ -13,23 +13,9 @@ list of items:
     * Drop code (the `Drop::drop` function is not called directly)
     * Drop implementations of types without an explicit `Drop` implementation
 
-The lowering is triggered by calling the [`mir_built`] query.
-There is an intermediate representation
-between [HIR] and [MIR] called the [THIR] that is only used during lowering.
-[THIR] means "Typed HIR" and used to be called "HAIR (High-level Abstract IR)".
-The [THIR]'s most important feature is that the various adjustments (which happen
-without explicit syntax) like coercions, autoderef, autoref and overloaded method
-calls have become explicit casts, deref operations, reference expressions or
-concrete function calls.
-
-The [THIR] is a shallow wrapper around [HIR], with datatypes that mirror the [HIR] datatypes.
-For example, instead of `-x` being a `thir::ExprKind::Neg(thir::Expr)`
-(a deep copy), it is a `thir::ExprKind::Neg(hir::Expr)` (a shallow copy).
-This shallowness enables the [THIR] to represent all datatypes that [HIR] has, but
-without having to create an in-memory copy of the entire [HIR].
-[MIR] lowering will first convert the topmost expression from
-[HIR] to [THIR] (in [`rustc_mir_build::thir::cx::expr`]) and then process
-the [THIR] expressions recursively.
+The lowering is triggered by calling the [`mir_built`] query. The MIR builder does
+not actually use the HIR but operates on the [THIR] instead, processing THIR
+expressions recursively.
 
 The lowering creates local variables for every argument as specified in the signature.
 Next, it creates local variables for every binding specified (e.g. `(a, b): (i32, String)`)
diff --git a/src/thir.md b/src/thir.md
new file mode 100644
index 000000000..b023eb2e2
--- /dev/null
+++ b/src/thir.md
@@ -0,0 +1,44 @@
+# The THIR
+
+<!-- toc -->
+
+The THIR ("Typed High-Level Intermediate Representation"), previously called HAIR for
+"High-Level Abstract IR", is another IR used by rustc that is generated after
+[type checking]. It is (as of <!-- date: 2021-03 --> March 2021) only used for
+[MIR construction] and [exhaustiveness checking], but
+[it may also soon be used for unsafety checking][thir-unsafeck] as a replacement
+for the current MIR unsafety checker.
+
+[type checking]: ./type-checking.md
+[MIR construction]: ./mir/construction.md
+[exhaustiveness checking]: ./pat-exhaustive-checking.md
+[thir-unsafeck]: https://github.com/rust-lang/compiler-team/issues/402
+
+As the name might suggest, the THIR is a lowered version of the [HIR] where all
+the types have been filled in, which is possible after type checking has completed.
+But it has some other interesting features that distinguish it from the HIR:
+
+- Like the MIR, the THIR only represents bodies, i.e. "executable code"; this includes
+  function bodies, but also `const` initializers, for example. Consequently, the THIR
+  has no representation for items like `struct`s or `trait`s.
+
+- Each body of THIR is only stored temporarily and is dropped as soon as it's no longer
+  needed, as opposed to being stored until the end of the compilation process (which
+  is what is done with the HIR).
+
+- Besides making the types of all nodes available, the THIR also has additional
+  desugaring compared to the HIR. For example, automatic references and dereferences
+  are made explicit, and method calls and overloaded operators are converted into
+  plain function calls. Destruction scopes are also made explicit.
+
+[HIR]: ./hir.md
+
+The THIR lives in [`rustc_mir_build::thir`][thir-docs]. To construct a [`thir::Expr`],
+you can use the [`build_thir`] function, passing in the memory arena where the THIR
+will be allocated. Dropping this arena will result in the THIR being destroyed,
+which is useful to keep peak memory in check. Having a THIR representation of
+all bodies of a crate in memory at the same time would be very heavy.
+
+[thir-docs]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/index.html
+[`thir::Expr`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/struct.Expr.html
+[`build_thir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/fn.build_thir.html