-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus. Whenever a term contains more than one
-redex, we have to choose which one to reduce, and this choice can make
-a difference. For instance, in the term `((\x.I)(ωω)`, if we reduce
-the leftmost redex first, the term reduces to the normal form `I` in
-one step. But if we reduce the left most redex instead (namely,
-`(ωω)`), we do not arrive at a normal form, and are in danger of
-entering an infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference. For instance,
+in the term `((\x.I)(ωω))`, if we reduce the leftmost redex first, the
+term reduces to the normal form `I` in one step. But if we reduce the
+left most redex instead (namely, `(ωω)`), we do not arrive at a normal
+form, and are in danger of entering an infinite loop.
+
+Thanks to the recent introduction of sum types (disjoint union), we are now