reformatting and corrections in part 2 (#105)

* wip

* wip

* wip

* explain companion objects and non-extension methods

* wip

* wip

* wip

* correct "type constructor" in chapter 5

* wip

* wip

* wip

* wip

* wip changes

* wip

* wip

* wip

* wip

sofp-src/lyx/sofp-applicative.lyx

@@ -367,7 +367,7 @@ flatMap
 
 \end_inset
 
- methods from sequences to other type constructors that support such methods
+ methods from sequences to other type constructors that support those methods
  obeying suitable laws.
  Following the same path, we now turn to the 
 \begin_inset listings
@@ -395,7 +395,7 @@ zip
 \end_inset
 
  is most often used with sequences, many other type constructors can also
- have a suitable 
+ have a lawful 
 \begin_inset listings
 inline true
 status open

sofp-src/lyx/sofp-curry-howard.lyx

@@ -5495,7 +5495,7 @@ status open
 
 \begin_layout Plain Layout
 
-F[A]
+F
 \end_layout
 
 \end_inset
@@ -25581,7 +25581,15 @@ decidable logic
  i.e., it has an algorithm that either finds a proof or disproves any given
  formula.
  However, that logic cannot handle type constructors such as 
-\begin_inset Formula $\text{Array}^{A}$
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+Array
+\end_layout
+
 \end_inset
 
 .
@@ -27426,7 +27434,7 @@ Solution
 \end_layout
 
 \begin_layout Standard
-Begin by defining a type alias for the type constructor 
+Begin by defining a type alias for the type 
 \begin_inset Formula $\text{Reader}^{E,A}$
 \end_inset
 
@@ -28658,7 +28666,7 @@ Solution
 
 \begin_layout Standard
 For a type constructor, say, 
-\begin_inset Formula $P^{A}$
+\begin_inset Formula $P$
 \end_inset
 
 , the standard type signatures for 
@@ -29918,7 +29926,7 @@ status open
 
 \begin_layout Plain Layout
 
-P[A]
+P
 \end_layout
 
 \end_inset
@@ -29969,7 +29977,7 @@ noprefix "false"
 
 \begin_layout Standard
 For the type constructor 
-\begin_inset Formula $Q^{T,A}$
+\begin_inset Formula $Q$
 \end_inset
 
  defined in Exercise

sofp-src/lyx/sofp-essay1.lyx

@@ -986,9 +986,9 @@ name "fig:The-Pyongyang-method-of-error-free-programming-1"
 \begin_layout Standard
 It is interesting to note that most older programming languages (C/C++,
  Java, JavaScript, Python) do not support some of these composite types.
- In other words, these programming languages have type systems based on
+ In other words, those programming languages have type systems based on
  an incomplete logic.
- As a result, users of these languages have to implement burdensome workarounds
+ As a result, users of those languages have to implement burdensome workarounds
  that make for error-prone code.
  Failure to follow mathematical principles has real costs (Figure
 \begin_inset space ~
@@ -1147,7 +1147,7 @@ industrial
 
  group are based on existing and mature software ecosystems: F# on .NET,
  Scala on JVM, and Swift on the MacOS/iOS platform.
- One of the important design requirements for these languages is 100% binary
+ One of the important design requirements for those languages is 100% binary
  compatibility with their 
 \begin_inset Quotes eld
 \end_inset
@@ -1226,13 +1226,20 @@ object-oriented programming
 \end_inset
 
  paradigm.
- At the same time, these new languages still have logically complete type
- systems, which gives developers an important benefit of type-safe domain
- modeling.
+ At the same time, those new 
+\begin_inset Quotes eld
+\end_inset
+
+industrial
+\begin_inset Quotes erd
+\end_inset
+
+ functional languages still have logically complete type systems, which
+ gives developers an important benefit of type-safe domain modeling.
 \end_layout
 
 \begin_layout Standard
-Nevertheless, the type systems of these languages are not equally powerful.
+Nevertheless, the type systems of those languages are not equally powerful.
  For instance, F# and Swift are similar to OCaml in many ways but omit OCaml's
  parameterized modules and some other features.
  Of all the mentioned languages, only Scala and Haskell directly support

sofp-src/lyx/sofp-essay2.lyx

@@ -2380,12 +2380,12 @@ literal "false"
 \begin_layout Standard
 Looking at the situation in construction business in the U.S.A., we find that
  it employs about 
-\begin_inset Formula $10$
+\begin_inset Formula $40$
 \end_inset
 
  times more construction workers as architects.
- We might conclude that perhaps one software engineer is required per dozen
- software artisans.
+ We might conclude that perhaps one software engineer is required per several
+ dozen software artisans.
 \end_layout
 
 \begin_layout Standard