minor fixes

src/plta/Connectives.lagda

@@ -8,15 +8,15 @@ permalink : /Connectives/
 module plta.Connectives where
 \end{code}
 
-This chapter introduces the basic logical connectives, by observing
+This chapter introduces the basic logical connectives, by observing a
-a correspondence between connectives of logic and data types,
+correspondence between connectives of logic and data types, a
-a principle known as *Propositions as Types*.
+principle known as _Propositions as Types_.
 
-+ *conjunction* is *product*
+  * _conjunction_ is _product_
-+ *disjunction* is *sum*
+  * _disjunction_ is _sum_
-+ *true* is *unit type*
+  * _true_ is _unit type_
-+ *false* is *empty type*
+  * _false_ is _empty type_
-+ *implication* is *function space*
+  * _implication_ is _function space_
 
 
 ## Imports

src/plta/Lambda.lagda

@@ -4,18 +4,18 @@ layout    : page
 permalink : /Lambda/
 ---
 
-*Add a couple of simpler examples* ``id · `zero`` and ``twoᶜ · sucᶜ · `zero``.
+*Todo: Experiment with defining variable names* smart constructor `` ƛ`_⇒_ ``
-
-*Experiment with defining variables* smart constructor `` ƛ`_⇒_ ``
 
 \begin{code}
 module plta.Lambda where
 \end{code}
 
+<!--
 [This chapter was originally based on Chapter _Stlc_
 of _Software Foundations_ (_Programming Language Foundations_).
 It has now been updated, but if you spot any plagiarism
 please let me know. – P]
+-->
 
 The _lambda-calculus_, first published by the logician Alonzo Church in
 1932, is a core calculus with only three syntactic constructs:

src/plta/Properties.lagda

@@ -1369,7 +1369,7 @@ det β-zero        β-zero            =  refl
 det (β-suc VL)    (ξ-case L—→L″)    =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
 det (β-suc _)     (β-suc _)         =  refl
 det β-μ           β-μ               =  refl
--- \end{code}
+\end{code}
 The proof is by induction over possible reductions.  We consider
 three typical cases.