move lambda and extensionality to Isomorphism, fix links

src/plta/Connectives.lagda

@@ -26,20 +26,12 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Data.Nat.Properties.Simple using (+-suc)
+open import Data.Nat.Properties using (+-suc)
 open import Function using (_∘_)
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
+open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
 open plta.Isomorphism.≃-Reasoning
 \end{code}
 
-We assume [extensionality][extensionality].
-\begin{code}
-postulate
-  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-\end{code}
-
-[extensionality]: ../Equality/index.html#extensionality
-
 
 ## Conjunction is product
 

src/plta/Decidable.lagda

@@ -33,7 +33,9 @@ open import Function using (_∘_)
 
 ## Evidence vs Computation
 
-Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}) defined comparison an inductive datatype, which provides *evidence* that one number is less than or equal to another.
+Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %})
+defined comparison an inductive datatype, which provides *evidence* that one number
+is less than or equal to another.
 \begin{code}
 infix 4 _≤_
 
@@ -62,11 +64,8 @@ data Bool : Set where
   true  : Bool
   false : Bool
 \end{code}
-We will use `true` to represent the case where a proposition holds,
-and `false` to represent the case where a proposition fails to hold.
-
 Given booleans, we can define a function of two numbers that
-*computes* to true if the comparison holds, and false otherwise.
+*computes* to `true` if the comparison holds and to `false` otherwise.
 \begin{code}
 infix 4 _≤ᵇ_
 
@@ -347,8 +346,8 @@ exactly when `m ≤ n` is inhabited.
 ≤→≤ᵇ′ = fromWitness
 \end{code}
 
-In summary, it is usually best to eschew booleans and rely on decidables instead.  If you
+In summary, it is usually best to eschew booleans and rely on decidables instead.
-need booleans, they and their properties are easily derived from the
+If you need booleans, they and their properties are easily derived from the
 corresponding decidables.
 
 ## Logical connectives

src/plta/Equality.lagda

@@ -114,7 +114,7 @@ Again, a useful exercise is to carry out an interactive development, checking
 how Agda's knowledge changes as each of the two arguments is
 instantiated.
 
-## Congruence and substitution
+## Congruence and substitution {#cong}
 
 Equality satisfies *congruence*.  If two terms are equal,
 they remain so after the same function is applied to both.
@@ -404,86 +404,6 @@ Nonetheless, rewrite is a vital part of the Agda toolkit,
 as earlier examples have shown.
 
 
-## Lambda expressions
-
-We pause for a moment to define *lambda expressions*, which provide a
-compact way to define functions without naming them, and will prove
-convenient in much of what follows.
-
-A term of the form
-
-    λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ }
-
-is equivalent to a function `f` defined by the equations
-
-    f P₁ = e₁
-    ⋯
-    f Pᵢ = eᵢ
-
-where the `Pᵢ` are patterns (left-hand sides of an equation) and the
-`Nᵢ` are expressions (right-hand side of an equation).
-
-In the case that the pattern is a variable, we may also use the syntax
-
-    λ x → N
-
-or
-
-    λ (x : A) → N
-
-both of which are equivalent to `λ{ x → N }`. The latter allows one to
-specify the domain of the function.
-
-Often using an anonymous lambda expression is more convenient than
-using a named function: it avoids a lengthy type declaration; and the
-definition appears exactly where the function is used, so there is no
-need for the writer to remember to declare it in advance, or for the
-reader to search for the definition elsewhere in the code.
-
-
-## Extensionality {#extensionality}
-
-Extensionality asserts that the only way to distinguish functions is
-by applying them; if two functions applied to the same argument always
-yield the same result, then they are the same functions.  It is the
-converse of `cong-app`, introduced earlier.
-
-Agda does not presume extensionality, but we can postulate that it holds.
-\begin{code}
-postulate
-  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-\end{code}
-Postulating extensionality does not lead to difficulties, as it is
-known to be consistent with the theory that underlies Agda.
-
-As an example, consider that we need results from two libraries,
-one where addition is defined as above, and one where it is
-defined the other way around.
-\begin{code}
-_+′_ : ℕ → ℕ → ℕ
-m +′ zero  = m
-m +′ suc n = suc (m +′ n)
-\end{code}
-Applying commutativity, it is easy to show that both operators always
-return the same result given the same arguments.
-\begin{code}
-same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
-same-app m n rewrite +-comm m n = helper m n
-  where
-  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
-  helper m zero    = refl
-  helper m (suc n) = cong suc (helper m n)
-\end{code}
-However, it might be convenient to assert that the two operators are
-actually indistinguishable. This we can do via two applications of
-extensionality.
-\begin{code}
-same : _+′_ ≡ _+_
-same = extensionality λ{m → extensionality λ{n → same-app m n}}
-\end{code}
-We will occasionally have need to postulate extensionality in what follows.
-
-
 ## Leibniz equality
 
 The form of asserting equivalence that we have used is due to Martin Löf,

src/plta/Isomorphism.lagda

@@ -21,8 +21,50 @@ distributivity.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong-app)
 open Eq.≡-Reasoning
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Nat.Properties using (+-comm)
 \end{code}
 
+
+## Lambda expressions
+
+The chapter begins with a few preliminaries that will be useful
+here and elsewhere: lambda expressions, function composition, and
+extensionality.
+
+*Lambda expressions* provide a compact way to define functions without
+naming them.  A term of the form
+
+    λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ }
+
+is equivalent to a function `f` defined by the equations
+
+    f P₁ = e₁
+    ⋯
+    f Pᵢ = eᵢ
+
+where the `Pᵢ` are patterns (left-hand sides of an equation) and the
+`Nᵢ` are expressions (right-hand side of an equation).
+
+In the case that there is one equation and the pattern is a variable,
+we may also use the syntax
+
+    λ x → N
+
+or
+
+    λ (x : A) → N
+
+both of which are equivalent to `λ{x → N}`. The latter allows one to
+specify the domain of the function.
+
+Often using an anonymous lambda expression is more convenient than
+using a named function: it avoids a lengthy type declaration; and the
+definition appears exactly where the function is used, so there is no
+need for the writer to remember to declare it in advance, or for the
+reader to search for the definition elsewhere in the code.
+
+
 ## Function composition
 
 In what follows, we will make use of function composition.
@@ -31,12 +73,62 @@ _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
 (g ∘ f) x  = g (f x)
 \end{code}
 Thus, `g ∘ f` is the function that first applies `f` and
-then applies `g`.
+then applies `g`.  An equivalent definition, exploiting lambda
+expressions, is as follows.
+\begin{code}
+_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
+g ∘′ f  =  λ x → g (f x)
+\end{code}
+
+
+## Extensionality {#extensionality}
+
+Extensionality asserts that the only way to distinguish functions is
+by applying them; if two functions applied to the same argument always
+yield the same result, then they are the same functions.  It is the
+converse of `cong-app`, as introduced
+[earlier]({{ site.baseurl }}{% link out/plta/Equality.md %}/#cong).
+
+Agda does not presume extensionality, but we can postulate that it holds.
+\begin{code}
+postulate
+  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
+\end{code}
+Postulating extensionality does not lead to difficulties, as it is
+known to be consistent with the theory that underlies Agda.
+
+As an example, consider that we need results from two libraries,
+one where addition is defined as in
+Chapter [Naturals]({{ site.baseurl }}{% link out/plta/Naturals.md %})
+and one where it is defined the other way around.
+\begin{code}
+_+′_ : ℕ → ℕ → ℕ
+m +′ zero  = m
+m +′ suc n = suc (m +′ n)
+\end{code}
+Applying commutativity, it is easy to show that both operators always
+return the same result given the same arguments.
+\begin{code}
+same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
+same-app m n rewrite +-comm m n = helper m n
+  where
+  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
+  helper m zero    = refl
+  helper m (suc n) = cong suc (helper m n)
+\end{code}
+However, it might be convenient to assert that the two operators are
+actually indistinguishable. This we can do via two applications of
+extensionality.
+\begin{code}
+same : _+′_ ≡ _+_
+same = extensionality (λ m → extensionality (λ n → same-app m n))
+\end{code}
+We will occasionally need to postulate extensionality in what follows.
 
 
 ## Isomorphism
 
-In set theory, two sets are isomorphic if they are in one-to-one correspondence.
+Two sets are isomorphic if they are in one-to-one correspondence.
 Here is a formal definition of isomorphism.
 \begin{code}
 infix 0 _≃_

src/plta/Lists.lagda

@@ -28,14 +28,6 @@ open import Level using (Level)
 open import plta.Isomorphism using (_≃_)
 \end{code}
 
-We assume [extensionality][extensionality].
-\begin{code}
-postulate
-  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-\end{code}
-
-[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
-
 
 ## Lists
 

src/plta/Modules.lagda

@@ -23,23 +23,15 @@ open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
 open import Relation.Nullary using (¬_)
 open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
-open import plta.Isomorphism using (_≃_)
 open import Function using (_∘_)
 open import Level using (Level)
 open import Data.Maybe using (Maybe; just; nothing)
 open import Data.List using (List; []; _∷_; _++_; map; foldr; downFrom)
 open import Data.List.All using (All; []; _∷_)
 open import Data.List.Any using (Any; here; there)
+open import plta.Isomorphism using (_≃_; extensionality)
 \end{code}
 
-We assume [extensionality][extensionality].
-\begin{code}
-postulate
-  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-\end{code}
-
-[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
-
 
 
 ## Modules

src/plta/Preface.lagda

@@ -78,7 +78,7 @@ Most of the text was written during a sabbatical in the first half of 2018.
 
 -- Philip Wadler, Rio de Janeiro, January--June 2018
 
-[tapl]: http://www.cis.upenn.edu/~bcpierce/tapl/index.html
+[tapl]: http://www.cis.upenn.edu/~bcpierce/tapl/
 [sf]: https://softwarefoundations.cis.upenn.edu/
 [ta]: http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf
 [stump]: http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908

src/plta/Quantifiers.lagda

@@ -22,17 +22,9 @@ open import Relation.Nullary using (¬_)
 open import Function using (_∘_)
 open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
+open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
 \end{code}
 
-We assume [extensionality][extensionality].
-\begin{code}
-postulate
-  extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-\end{code}
-
-[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality
-
 
 ## Universals
 
@@ -217,7 +209,7 @@ The result can be viewed as a generalisation of currying.  Indeed, the code to
 establish the isomorphism is identical to what we wrote when discussing
 [implication][implication].
 
-[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/index.html#implication
+[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/#implication
 
 ### Exercise (`∃-distrib-⊎`)