--> τ</code>. This looks like logical implication. Let's take
-that resemblance seriously. Then note that types respect modus
-ponens: given two expressions <code>fn:(σ -> τ)</code> and
-<code>arg:σ</code>, the application of `fn` to `arg` has type
-<code>(fn arg):τ</code>.
+-> τ</code>. This looks like logical implication. We'll take
+that resemblance seriously when we discuss the Curry-Howard
+correspondence. In the meantime, note that types respect modus
+ponens: