diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index e355c89196..8f979c6090 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -5,6 +5,12 @@
 
 # Language Manual
 
+- [Dependent Types](./deptypes.md)
+  - [Simple Type Theory](./simptypes.md)
+  - [Types as objects](./typeobjs.md)
+  - [Function Abstraction and Evaluation](./funabst.md)
+  - [Introducing Definitions](./introdef.md)
+  - [What makes dependent type theory dependent?](./dep.md)
 - [Functions](./functions.md)
 - [Sections](./sections.md)
 - [Namespaces](./namespaces.md)
diff --git a/doc/dep.md b/doc/dep.md
new file mode 100644
index 0000000000..07173516e8
--- /dev/null
+++ b/doc/dep.md
@@ -0,0 +1,66 @@
+## What makes dependent type theory dependent?
+
+The short explanation is that what makes dependent type theory dependent is that types can depend on parameters.
+You have already seen a nice example of this: the type ``List α`` depends on the argument ``α``, and
+this dependence is what distinguishes ``List Nat`` and ``List Bool``.
+For another example, consider the type ``Vector α n``, the type of vectors of elements of ``α`` of length ``n``.
+This type depends on *two* parameters: the type ``α : Type`` of the elements in the vector and the length ``n : Nat``.
+
+Suppose we wish to write a function ``cons`` which inserts a new element at the head of a list.
+What type should ``cons`` have? Such a function is *polymorphic*: we expect the ``cons`` function for ``Nat``, ``Bool``,
+or an arbitrary type ``α`` to behave the same way.
+So it makes sense to take the type to be the first argument to ``cons``, so that for any type, ``α``, ``cons α``
+is the insertion function for lists of type ``α``. In other words, for every ``α``, ``cons α`` is the function that takes an element ``a : α``
+and a list ``as : List α``, and returns a new list, so we have ``cons α a as : list α``.
+
+It is clear that ``cons α`` should have type ``α → List α → List α``. But what type should ``cons`` have?
+A first guess might be ``Type → α → list α → list α``, but, on reflection, this does not make sense:
+the ``α`` in this expression does not refer to anything, whereas it should refer to the argument of type ``Type``.
+In other words, *assuming* ``α : Type`` is the first argument to the function, the type of the next two elements are ``α`` and ``List α``.
+These types vary depending on the first argument, ``α``.
+
+This is an instance of a *dependent function type*, or *dependent arrow type*. Given ``α : Type`` and ``β : α → Type``,
+think of ``β`` as a family of types over ``α``, that is, a type ``β a`` for each ``a : α``.
+In that case, the type ``(x : α) → β x`` denotes the type of functions ``f`` with the property that,
+for each ``a : α``, ``f a`` is an element of ``β a``. In other words, the type of the value returned by ``f`` depends on its input.
+
+Notice that ``(x : α) → β`` makes sense for any expression ``β : Type``. When the value of ``β`` depends on ``x``
+(as does, for example, the expression ``β x`` in the previous paragraph), ``(x : α) → β`` denotes a dependent function type.
+When ``β`` doesn't depend on ``x``, ``(x : α) → β`` is no different from the type ``α → β``.
+Indeed, in dependent type theory (and in Lean), ``α → β`` is just notation for ``(x : α) → β`` when ``β`` does not depend on ``x``.
+
+Returning to the example of lists, we can use the command `#check` to inspect the type of the following `List` functions
+We will explain the ``@`` symbol and the difference between the round and curly brackets momentarily.
+
+```lean
+#check @List.cons    -- {α : Type u_1} → α → List α → List α
+#check @List.nil     -- {α : Type u_1} → List α
+#check @List.length  -- {α : Type u_1} → List α → Nat
+#check @List.append  -- {α : Type u_1} → List α → List α → List α
+```
+
+Just as dependent function types ``(x : α) → β x`` generalize the notion of a function type ``α → β`` by allowing ``β`` to depend on ``α``,
+dependent cartesian product types ``(x : α) × β x`` generalize the cartesian product ``α × β`` in the same way. Dependent products are also
+called *sigma* types, and you can also write them as `Σ x : α, β x`. You can use `⟨a, b⟩` or `Sigma.mk a b` to create a dependent pair.
+
+```lean
+universes u v
+
+def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (x : α) × β x :=
+  ⟨a, b⟩
+
+def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ x : α, β x :=
+  Sigma.mk a b
+
+#reduce f
+#reduce g
+
+#reduce f Type (fun α => α) Nat 10
+#reduce g Type (fun α => α) Nat 10
+
+#reduce (f Type (fun α => α) Nat 10).1 -- Nat
+#reduce (g Type (fun α => α) Nat 10).1 -- Nat
+#reduce (f Type (fun α => α) Nat 10).2 -- 10
+#reduce (g Type (fun α => α) Nat 10).2 -- 10
+```
+The function `f` and `g` above denote the same function.
diff --git a/doc/deptypes.md b/doc/deptypes.md
new file mode 100644
index 0000000000..a7c5932946
--- /dev/null
+++ b/doc/deptypes.md
@@ -0,0 +1,3 @@
+# Dependent Types
+
+In this section, we introduce simple type theory, types as objects, definitions, and explain what makes dependent type theory *dependent*.
diff --git a/doc/funabst.md b/doc/funabst.md
new file mode 100644
index 0000000000..bab719ebef
--- /dev/null
+++ b/doc/funabst.md
@@ -0,0 +1,145 @@
+## Function Abstraction and Evaluation
+
+We have seen that if we have ``m n : Nat``, then we have ``(m, n) : Nat × Nat``.
+This gives us a way of creating pairs of natural numbers.
+Conversely, if we have ``p : Nat × Nat``, then
+we have ``p.1 : Nat`` and ``p.2 : Nat``.
+This gives us a way of "using" a pair, by extracting its two components.
+
+We already know how to "use" a function ``f : α → β``, namely,
+we can apply it to an element ``a : α`` to obtain ``f a : β``.
+But how do we create a function from another expression?
+
+The companion to application is a process known as "lambda abstraction."
+Suppose that giving a variable ``x : α`` we can construct an expression ``t : β``.
+Then the expression ``fun (x : α) => t``, or, equivalently, ``λ (x : α) => t``, is an object of type ``α → β``.
+Think of this as the function from ``α`` to ``β`` which maps any value ``x`` to the value ``t``,
+which depends on ``x``.
+
+```lean
+#check fun (x : Nat) => x + 5
+#check λ (x : Nat) => x + 5
+#check fun x : Nat => x + 5
+#check λ x : Nat => x + 5
+```
+
+Here are some more examples:
+
+```lean
+constant f : Nat → Nat
+constant h : Nat → Bool → Nat
+
+#check fun x : Nat => fun y : Bool => h (f x) y   -- Nat → Bool → Nat
+#check fun (x : Nat) (y : Bool) => h (f x) y      -- Nat → Bool → Nat
+#check fun x y => h (f x) y                       -- Nat → Bool → Nat
+```
+
+Lean interprets the final three examples as the same expression; in the last expression,
+Lean infers the type of ``x`` and ``y`` from the types of ``f`` and ``h``.
+
+Some mathematically common examples of operations of functions can be described in terms of lambda abstraction:
+
+```lean
+constant f : Nat → String
+constant g : String → Bool
+constant b : Bool
+
+#check fun x : Nat => x        -- Nat → Nat
+#check fun x : Nat => b        -- Nat → Bool
+#check fun x : Nat => g (f x)  -- Nat → Bool
+#check fun x => g (f x)        -- Nat → Bool
+```
+
+Think about what these expressions mean. The expression ``fun x : Nat => x`` denotes the identity function on ``Nat``,
+the expression ``fun x : α => b`` denotes the constant function that always returns ``b``,
+and ``fun x : Nat => g (f x)``, denotes the composition of ``f`` and ``g``.
+We can, in general, leave off the type annotations on the variable and let Lean infer it for us.
+So, for example, we can write ``fun x => g (f x)`` instead of ``fun x : Nat => g (f x)``.
+
+We can abstract over the constants `f` and `g` in the previous definitions:
+
+```lean
+#check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
+-- (String → Bool) → (Nat → String) → Nat → Bool
+```
+
+We can also abstract over types:
+
+```lean
+#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
+```
+The last expression, for example, denotes the function that takes three types, ``α``, ``β``, and ``γ``, and two functions, ``g : β → γ`` and ``f : α → β``, and returns the composition of ``g`` and ``f``. (Making sense of the type of this function requires an understanding of dependent products, which we will explain below.) Within a lambda expression ``fun x : α => t``, the variable ``x`` is a "bound variable": it is really a placeholder, whose "scope" does not extend beyond ``t``.
+For example, the variable ``b`` in the expression ``fun (b : β) (x : α) => b`` has nothing to do with the constant ``b`` declared earlier.
+In fact, the expression denotes the same function as ``fun (u : β) (z : α), u``. Formally, the expressions that are the same up to a renaming of bound variables are called *alpha equivalent*, and are considered "the same." Lean recognizes this equivalence.
+
+Notice that applying a term ``t : α → β`` to a term ``s : α`` yields an expression ``t s : β``.
+Returning to the previous example and renaming bound variables for clarity, notice the types of the following expressions:
+
+```lean
+#check (fun x : Nat => x) 1     -- Nat
+#check (fun x : Nat => true) 1  -- Bool
+
+constant f : Nat → String
+constant g : String → Bool
+
+#check
+  (fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)) Nat String Bool g f 0
+  -- Bool
+```
+
+As expected, the expression ``(fun x : Nat =>  x) 1`` has type ``Nat``.
+In fact, more should be true: applying the expression ``(fun x : Nat => x)`` to ``1`` should "return" the value ``1``. And, indeed, it does:
+
+```lean
+#reduce (fun x : Nat => x) 1     -- 1
+#reduce (fun x : Nat => true) 1  -- true
+
+constant f : Nat → String
+constant g : String → Bool
+
+#reduce
+  (fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)) Nat String Bool g f 0
+  -- g (f 0)
+```
+
+The command ``#reduce`` tells Lean to evaluate an expression by *reducing* it to its normal form,
+which is to say, carrying out all the computational reductions that are sanctioned by its kernel.
+The process of simplifying an expression ``(fun x => t) s`` to ``t[s/x]`` -- that is, ``t`` with ``s`` substituted for the variable ``x`` --
+is known as *beta reduction*, and two terms that beta reduce to a common term are called *beta equivalent*.
+But the ``#reduce`` command carries out other forms of reduction as well:
+
+```lean
+constant m : Nat
+constant n : Nat
+constant b : Bool
+
+#reduce (m, n).1        -- m
+#reduce (m, n).2        -- n
+
+#reduce true && false   -- false
+#reduce false && b      -- false
+#reduce b && false      -- Bool.rec false false b
+
+#reduce n + 0           -- n
+#reduce n + 2           -- Nat.succ (Nat.succ n)
+#reduce 2 + 3           -- 5
+```
+
+We explain later how these terms are evaluated.
+For now, we only wish to emphasize that this is an important feature of dependent type theory:
+every term has a computational behavior, and supports a notion of reduction, or *normalization*.
+In principle, two terms that reduce to the same value are called *definitionally equal*.
+They are considered "the same" by Lean's type checker, and Lean does its best to recognize and support these identifications.
+The `#reduce` command is mainly useful to understand why two terms are considered the same.
+
+Lean is also a programming language. It has a compiler to native code and an interpreter.
+You can use the command `#eval` to execute expressions, and it is the preferred way of testing your functions.
+Note that `#eval` and `#reduce` are *not* equivalent. The command `#eval` first compiles Lean expressions
+into an intermediate representation (IR) and then uses an interpreter to execute the generated IR.
+Some builtin types (e.g., `Nat`, `String`, `Array`) have a more efficient representation in the IR.
+The IR has support for using foreign functions that are opaque to Lean.
+
+In contrast, the ``#reduce`` command relies on a reduction engine similar to the one used in Lean's trusted kernel,
+the part of Lean that is responsible for checking and verifying the correctness of expressions and proofs.
+It is less efficient than ``#eval``, and treats all foreign functions as opaque constants.
+We later discuss other differences between the two commands.
diff --git a/doc/introdef.md b/doc/introdef.md
new file mode 100644
index 0000000000..64696e82bf
--- /dev/null
+++ b/doc/introdef.md
@@ -0,0 +1,66 @@
+## Introducing Definitions
+
+The ``def`` command provides one important way of defining new objects.
+
+```lean
+
+def foo : (Nat → Nat) → Nat :=
+  fun f => f 0
+
+#check foo   -- (Nat → Nat) → Nat
+#print foo
+```
+
+We can omit the type when Lean has enough information to infer it:
+
+```lean
+def foo :=
+  fun (f : Nat → Nat) => f 0
+```
+
+The general form of a definition is ``def foo : α := bar``. Lean can usually infer the type ``α``, but it is often a good idea to write it explicitly.
+This clarifies your intention, and Lean will flag an error if the right-hand side of the definition does not have the right type.
+
+Lean also allows us to use an alternative format that puts the abstracted variables before the colon and omits the lambda:
+```lean
+def double (x : Nat) : Nat :=
+  x + x
+
+#print double
+#check double 3
+#reduce double 3  -- 6
+#eval double 3    -- 6
+
+def square (x : Nat) :=
+  x * x
+
+#print square
+#check square 3
+#reduce square 3  -- 9
+#eval square 3    -- 9
+
+def doTwice (f : Nat → Nat) (x : Nat) : Nat :=
+  f (f x)
+
+#eval doTwice double 2   -- 8
+```
+
+These definitions are equivalent to the following:
+
+```lean
+def double : Nat → Nat :=
+  fun x => x + x
+
+def square : Nat → Nat :=
+  fun x => x * x
+
+def doTwice : (Nat → Nat) → Nat → Nat :=
+  fun f x => f (f x)
+```
+
+We can even use this approach to specify arguments that are types:
+
+```lean
+def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
+  g (f x)
+```
diff --git a/doc/simptypes.md b/doc/simptypes.md
new file mode 100644
index 0000000000..6bf803cd08
--- /dev/null
+++ b/doc/simptypes.md
@@ -0,0 +1,91 @@
+## Simple Type Theory
+
+"Type theory" gets its name from the fact that every expression has an associated *type*.
+For example, in a given context, ``x + 0`` may denote a natural number and ``f`` may denote a function on the natural numbers.
+For those that don't like math, a Lean natural number is an arbitrary precision unsigned integer.
+
+Here are some examples of how we can declare objects in Lean and check their types.
+
+```lean
+/- declare some constants -/
+
+constant m  : Nat   -- m is a natural number
+constant n  : Nat
+constant b1 : Bool  -- b1 is a Boolean
+constant b2 : Bool
+
+/- check their types -/
+
+#check m            -- output: Nat
+#check n
+#check n + 0        -- Nat
+#check m * (n + 0)  -- Nat
+#check b1           -- Bool
+#check b1 && b2     -- "&&" is the Boolean and
+#check b1 || b2     -- Boolean or
+#check true         -- Boolean "true"
+```
+
+Any text between the ``/-`` and ``-/`` constitutes a comment that is ignored by Lean.
+Similarly, two dashes indicate that the rest of the line contains a comment that is also ignored.
+Comment blocks can be nested, making it possible to "comment out" chunks of code, just as in many programming languages.
+
+The ``constant`` command introduce new constant symbols into the working environment.
+The ``#check`` command asks Lean to report their types; in Lean, commands that query the system for
+information typically begin with the hash symbol. You should try declaring some constants and type checking
+some expressions on your own. Declaring new objects in this way is a good way to experiment with the system.
+
+What makes simple type theory powerful is that one can build new types out of others.
+For example, if ``a`` and ``b`` are types, ``a -> b`` denotes the type of functions from ``a`` to ``b``,
+and ``a × b`` denotes the type of pairs consisting of an element of ``a``
+paired with an element of ``b``, it is also known as the *cartesian product*.
+Note that, `×` is an Unicode symbol. We believe that judicious use of Unicode improves legibility,
+and all moderns editors have great support for it. In the Lean standard library, we often use
+greek letters to denote types, and the Unicode symbol `→` as a more compact version of `->`.
+
+```lean
+constant m : Nat
+constant n : Nat
+
+constant f  : Nat → Nat         -- type the arrow as "\to" or "\r"
+constant f' : Nat -> Nat        -- alternative ASCII notation
+constant p  : Nat × Nat         -- type the product as "\times"
+constant q  : Prod Nat Nat      -- alternative notation
+constant g  : Nat → Nat → Nat
+constant g' : Nat → (Nat → Nat) -- has the same type as g!
+constant h  : Nat × Nat → Nat
+constant F  : (Nat → Nat) → Nat -- a "functional"
+
+#check f            -- Nat → Nat
+#check f n          -- Nat
+#check g m n        -- Nat
+#check g m          -- Nat → Nat
+#check (m, n)       -- Nat × Nat
+#check p.1          -- Nat
+#check p.2          -- Nat
+#check (m, n).1     -- Nat
+#check (p.1, n)     -- Nat × Nat
+#check F f          -- Nat
+```
+
+Once again, you should try some examples on your own.
+
+Let us dispense with some basic syntax. You can enter the unicode arrow ``→`` by typing ``\to`` or ``\r``.
+You can also use the ASCII alternative ``->``, so that the expression ``Nat -> Nat`` and ``Nat → Nat`` mean the same thing.
+Both expressions denote the type of functions that take a natural number as input and return a natural number as output.
+The unicode symbol ``×`` for the cartesian product is entered ``\times``.
+We will generally use lower-case greek letters like ``α``, ``β``, and ``γ`` to range over types.
+You can enter these particular ones with ``\a``, ``\b``, and ``\g``.
+
+There are a few more things to notice here. First, the application of a function ``f`` to a value ``x`` is denoted ``f x``.
+Second, when writing type expressions, arrows associate to the *right*; for example, the type of ``g`` is ``Nat → (Nat → Nat)``.
+Thus we can view ``g`` as a function that takes natural numbers and returns another function that takes a natural number and
+returns a natural number.
+In type theory, this is generally more convenient than writing ``g`` as a function that takes a pair of natural numbers as input,
+and returns a natural number as output. For example, it allows us to "partially apply" the function ``g``.
+The example above shows that ``g m`` has type ``Nat → Nat``, that is, the function that "waits" for a second argument, ``n``,
+and then returns ``g m n``. Taking a function ``h`` of type ``Nat × Nat → Nat`` and "redefining" it to look like ``g`` is a process
+known as *currying*, something we will come back to below.
+
+By now you may also have guessed that, in Lean, ``(m, n)`` denotes the ordered pair of ``m`` and ``n``,
+and if ``p`` is a pair, ``p.1`` and ``p.2`` denote the two projections.
diff --git a/doc/typeobjs.md b/doc/typeobjs.md
new file mode 100644
index 0000000000..35095f49e2
--- /dev/null
+++ b/doc/typeobjs.md
@@ -0,0 +1,115 @@
+## Types as objects
+
+One way in which Lean's dependent type theory extends simple type theory is that types themselves --- entities like ``Nat`` and ``Bool`` ---
+are first-class citizens, which is to say that they themselves are objects. For that to be the case, each of them also has to have a type.
+
+```lean
+#check Nat               -- Type
+#check Bool              -- Type
+#check Nat → Bool        -- Type
+#check Nat × Bool        -- Type
+#check Nat → Nat         -- ...
+#check Nat × Nat → Nat
+#check Nat → Nat → Nat
+#check Nat → (Nat → Nat)
+#check Nat → Nat → Bool
+#check (Nat → Nat) → Nat
+```
+
+We see that each one of the expressions above is an object of type ``Type``. We can also declare new constants and constructors for types:
+
+```lean
+constant α : Type
+constant β : Type
+constant F : Type → Type
+constant G : Type → Type → Type
+
+#check α        -- Type
+#check F α      -- Type
+#check F Nat    -- Type
+#check G α      -- Type → Type
+#check G α β    -- Type
+#check G α Nat  -- Type
+```
+
+Indeed, we have already seen an example of a function of type ``Type → Type → Type``, namely, the Cartesian product.
+
+```lean
+constant α : Type
+constant β : Type
+
+#check Prod α β       -- Type
+#check Prod Nat Nat   -- Type
+```
+
+Here is another example: given any type ``α``, the type ``List α`` denotes the type of lists of elements of type ``α``.
+
+```lean
+constant α : Type
+
+#check List α    -- Type
+#check List Nat  -- Type
+```
+
+Given that every expression in Lean has a type, it is natural to ask: what type does ``Type`` itself have?
+
+```lean
+#check Type      -- Type 1
+```
+
+We have actually come up against one of the most subtle aspects of Lean's typing system.
+Lean's underlying foundation has an infinite hierarchy of types:
+
+```lean
+#check Type     -- Type 1
+#check Type 1   -- Type 2
+#check Type 2   -- Type 3
+#check Type 3   -- Type 4
+#check Type 4   -- Type 5
+```
+
+Think of ``Type 0`` as a universe of "small" or "ordinary" types.
+``Type 1`` is then a larger universe of types, which contains ``Type 0`` as an element,
+and ``Type 2`` is an even larger universe of types, which contains ``Type 1`` as an element.
+The list is indefinite, so that there is a ``Type n`` for every natural number ``n``.
+``Type`` is an abbreviation for ``Type 0``:
+
+```lean
+#check Type
+#check Type 0
+```
+
+There is also another type, ``Prop``, which has special properties.
+
+```lean
+#check Prop -- Type
+```
+
+We will discuss ``Prop`` later.
+
+We want some operations, however, to be *polymorphic* over type universes. For example, ``List α`` should
+make sense for any type ``α``, no matter which type universe ``α`` lives in. This explains the type annotation of the function ``List``:
+
+```lean
+#check List    -- Type u_1 → Type u_1
+```
+
+Here ``u_1`` is a variable ranging over type levels. The output of the ``#check`` command means that whenever ``α`` has type ``Type n``, ``list α`` also has type ``Type n``. The function ``Prod`` is similarly polymorphic:
+
+```lean
+#check Prod    -- Type u_1 → Type u_2 → Type (max u_1 u_2)
+```
+
+To define polymorphic constants and variables, Lean allows us to declare universe variables explicitly:
+
+```lean
+universe u
+constant α : Type u
+#check α
+```
+Equivalently, we can write ``Type _`` to avoid giving the arbitrary universe a name:
+
+```lean
+constant α : Type _
+#check α
+```