minor changes to Prelude

index.md

@@ -6,13 +6,15 @@ layout : page
 This book is an introduction to programming language theory, written
 in Agda.  The authors are [Wen Kokke][wen] and [Philip Wadler][phil].
 
-Please send us comments!  The text is currrently being drafted. The
-first draft of Part I will be completed before the end of
-March 2018. When that is done it will be announced here, and that would be
-an excellent time to comment on the first part.
+Please send us comments!  The text is currrently being drafted.  Part I
+is ready for comment. We plan that Part II will be ready for comment
+by the end of May.
+
+Comments on all matters---organisation, material we should add,
+material we should remove, parts that require better explanation, good
+exercises, errors, and typos---are welcome.  Pull requests for small
+fixes are encouraged.
 
-The book was inspired by [Software Foundations][sf], but presents the
-material in a different way; see the [Preface](Preface).
 
 ## Front matter
 
@@ -20,6 +22,8 @@ material in a different way; see the [Preface](Preface).
 
 ## Part 1: Logical Foundations
 
+(This part is ready for review. Please send your comments!)
+
   - [Naturals: Natural numbers](Naturals)
   - [Properties: Proof by induction](Properties)
   - [Relations: Inductive Definition of Relations](Relations)
@@ -31,13 +35,10 @@ material in a different way; see the [Preface](Preface).
   - [Lists: Lists and higher-order functions](Lists)
   - [Decidable: Booleans and decision procedures](Decidable)
 
-  - [PropertiesAns: Solutions to exercises](PropertiesAns) 
-  - [RelationsAns: Solutions to exercises](RelationsAns) 
-  - [LogicAns: Solutions to exercises](LogicAns)
-  - [ListsAns: Solutions to exercises](ListsAns)
-
 ## Part 2: Programming Language Foundations
 
+(This part is not yet ready for review.)
+
   - [Maps: Total and Partial Maps](Maps)
   - [Stlc: The Simply Typed Lambda-Calculus](Stlc)
   - [StlcProp: Properties of STLC](StlcProp)

src/Equality.lagda

@@ -560,18 +560,18 @@ The answer is *universe polymorphism*, where a definition is made
 with respect to an arbitrary level `ℓ`. To make use of levels, we
 first import the following.
 \begin{code}
-open import Level using (Level; suc; zero; _⊔_)
+open import Level using (Level; _⊔_) renaming (suc to lsuc; zero to lzero)
 \end{code}
-Levels are isomorphic to natural numbers, and have the same constructors:
+Levels are isomorphic to natural numbers, and have similar constructors:
 
-    zero : Level
-    suc  : Level → Level
+    lzero : Level
+    lsuc  : Level → Level
 
 The names `Set₀`, `Set₁`, `Set₂` and so on are abbreviations for
 
-    Set zero
-    Set (suc zero)
-    Set (suc (suc zero))
+    Set lzero
+    Set (lsuc lzero)
+    Set (lsuc (lsuc lzero))
 
 and so on. There is also an operator
 
@@ -595,8 +595,8 @@ equality, are generalised to arbitrary levels as above.
 
 Here is the generalised definition of Leibniz equality.
 \begin{code}
-_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (suc ℓ)
-_≐′_ {A} x y = ∀ (P : A → Set ℓ) → P x → P y
+_≐′_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
+_≐′_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y
 \end{code}
 Before the signature used `Set₁` as the type of a term that includes
 `Set`, whereas here the signature uses `Set (suc ℓ)` as the type of a

src/Isomorphism.lagda

@@ -17,7 +17,6 @@ distributivity.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong-app)
 open Eq.≡-Reasoning
-open Level
 \end{code}
 
 ## Function composition

src/Preface.lagda

@@ -7,19 +7,24 @@ permalink : /Preface
 This book is an introduction to programming language theory, written
 in Agda.  The authors are [Wen Kokke][wen] and [Philip Wadler][phil].
 
-Please send us comments!  The text is currrently being drafted. The
-first draft of Part I will be completed before the end of
-March 2018. When that is done it will be announced here, and that would be
+Please send us comments!  The text is currrently being drafted.  Part I
+is ready for comment. We plan that Part II will be ready for comment
+by the end of May.
+
+Comments on all matters---organisation, material we should add,
+material we should remove, parts that require better explanation, good
+exercises, errors, and typos---are welcome.  Pull requests for small
+fixes are encouraged.
+
+<!--
+The first draft of Part I will be completed before the end of March
+2018. When that is done it will be announced here, and that would be
 an excellent time to comment on the first part.
+-->
 
 
 ## Personal remarks: From TAPL to PLTA
 
-I, along with many others, am a fan of Peirce's [Types and Programming
-Languages][tapl], known by the acronym TAPL. One of my best students
-started writing his own systems with no help from me, trained by that
-book.
-
 Since 2013, I have taught a course on Types and Semantics for
 Programming Languages to fourth-year undergraduates and masters
 students at the University of Edinburgh.  That course is not based on

src/extra/Extra.lagda

@@ -1,5 +1,3 @@
-<!--
-
 ## Disjunction
 
 In order to state totality, we need a way to formalise disjunction,
@@ -22,4 +20,22 @@ infixr 1 _⊎_
 \end{code}
 Thus, `m ≤ n ⊎ n ≤ m` parses as `(m ≤ n) ⊎ (n ≤ m)`.
 
--->
+------------------------------------------------------------------------
+
+I, along with many others, am a fan of Peirce's [Types and Programming
+Languages][tapl], known by the acronym TAPL. One of my best students
+started writing his own systems with no help from me, trained by that
+book.
+
+------------------------------------------------------------------------
+
+\begin{code}
+postulate
+  extensionality : ∀ {A B : Set} → {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
+
+extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
+extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
+\end{code}
+
+
+

src/extra/extra.agda

@@ -1,6 +0,0 @@
-postulate
-  extensionality : ∀ {A B : Set} → {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
-
-extensionality2 : ∀ {A B C : Set} → {f g : A → B → C} → (∀ (x : A) (y : B) → f x y ≡ g x y) → f ≡ g
-extensionality2 fxy≡gxy = extensionality (λ x → extensionality (λ y → fxy≡gxy x y))
-