moving plta to plfa

Notes.md

@@ -81,6 +81,11 @@ The following comments were collected on the Agda mailing list.
     - https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda
   + also cites Abel's habilitation
     -  http://www.cse.chalmers.se/~abela/habil.pdf
+  + See his note to the Agda mailing list of 26 June,
+	"Typed Jigger in vanilla Agda"
+    It points to the following solution.
+    - https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda
+  
 
 * András Kovács <kovacsahun@hotmail.com>
   + applies unary parametricity

_config.yml

@@ -1,6 +1,5 @@
 title: >
-  Code the Infinite:
+  Programming Language Foundations in Agda
-  Programming Languages in Agda
 
 # the author field should not be used in the template
 author: Wen Kokke
@@ -18,7 +17,7 @@ contributors:
     twitter_username: philipwadler
 
 description: > 
-  Programming Languages in Agda.
+  Programming Language Foundations in Agda
 
 # include disqus to allow comments e.d.
 disqus:

src/plfa/plta/Connectives.lagda

@@ -5,7 +5,7 @@ permalink : /Connectives/
 ---
 
 \begin{code}
-module plta.Connectives where
+module plfa.Connectives where
 \end{code}
 
 This chapter introduces the basic logical connectives, by observing a

src/plfa/plta/DeBruijn.lagda

@@ -5,7 +5,7 @@ permalink : /DeBruijn/
 ---
 
 \begin{code}
-module plta.DeBruijn where
+module plfa.DeBruijn where
 \end{code}
 
 The previous two chapters introduced lambda calculus, with a

src/plfa/plta/Decidable.lagda

@@ -5,7 +5,7 @@ permalink : /Decidable/
 ---
 
 \begin{code}
-module plta.Decidable where
+module plfa.Decidable where
 \end{code}
 
 We have a choice as to how to represent relations:

src/plfa/plta/Equality.lagda

@@ -5,7 +5,7 @@ permalink : /Equality/
 ---
 
 \begin{code}
-module plta.Equality where
+module plfa.Equality where
 \end{code}
 
 Much of our reasoning has involved equality.  Given two terms `M`

src/plfa/plta/Fonts.lagda

@@ -4,10 +4,6 @@ layout    : page
 permalink : /Fonts/
 ---
 
-\begin{code}
-module plta.Fonts where
-\end{code}
-
 Test page for fonts. All vertical bars should line up.
 
 \begin{code}
@@ -17,7 +13,8 @@ abcdefghijklmnopqrstuvwxyz|
 ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
 ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-ₐ   ₑ   ᵢⱼ    ₒ  ᵣ  ᵤ  ₓ  |
+ₐ   ₑ   ᵢⱼ    ₒ  ᵣₛₜᵤ  ₓ  |
+𝔸𝔹ℂ𝔻𝔼𝔽𝔾ℍ𝕀𝕁𝕂𝕃𝕄ℕ𝕆ℙℚℝ𝕊𝕋𝕌𝕍𝕎𝕏𝕐ℤ|
 --------------------------|
 ----------|
 0123456789|
@@ -29,23 +26,42 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
 ------------------------|
 ----|
+ℕℕℕℕ|
 ∀∀∃∃|
 ƛƛ··|
+′′″″|
+‴‴⁗⁗|
+††‡‡|
+''""|
+``~~|
 ≡≡≢≢|
+≃≃≲≲|
 ≟≟≐≐|
 ⟨⟨⟩⟩|
 ⌊⌊⌋⌋|
 ⌈⌈⌉⌉|
 →→⇒⇒|
 ←←⇐⇐|
-↦↦↠↠|
+——↠↠|
 ∈∈∋∋|
 ⊢⊢⊣⊣|
+∷∷∷∷|
+⦂⦂⦂⦂|
 ----|
 -}
 \end{code}
 
-Here are some characters that are not required to be monospaced.
+Here are some characters that are exactly two spaces wide.
+\begin{code}
+{-
+----|
+😇😇|
+😈😈|
+----|
+-}
+\end{code}
+
+Here are some characters that are not used because they are not monospaced.
 
 \begin{code}
 {-

src/plfa/plta/Induction.lagda

@@ -5,7 +5,7 @@ permalink : /Induction/
 ---
 
 \begin{code}
-module plta.Induction where
+module plfa.Induction where
 \end{code}
 
 > Induction makes you feel guilty for getting something out of nothing

src/plfa/plta/Inference.lagda

@@ -5,7 +5,7 @@ permalink : /Inference/
 ---
 
 \begin{code}
-module plta.Inference where
+module plfa.Inference where
 \end{code}
 
 

src/plfa/plta/Isomorphism.lagda

@@ -5,7 +5,7 @@ permalink : /Isomorphism/
 ---
 
 \begin{code}
-module plta.Isomorphism where
+module plfa.Isomorphism where
 \end{code}
 
 This section introduces isomorphism as a way of asserting that two

src/plfa/plta/Lambda.lagda

@@ -7,7 +7,7 @@ permalink : /Lambda/
 *Todo: Experiment with defining variable names* smart constructor `` ƛ`_⇒_ ``
 
 \begin{code}
-module plta.Lambda where
+module plfa.Lambda where
 \end{code}
 
 <!--

src/plfa/plta/Lists.lagda

@@ -5,7 +5,7 @@ permalink : /Lists/
 ---
 
 \begin{code}
-module plta.Lists where
+module plfa.Lists where
 \end{code}
 
 This chapter discusses the list data type.  It gives further examples

src/plfa/plta/Modules.lagda

@@ -8,7 +8,7 @@ permalink : /Modules/
 from the standard library. **
 
 \begin{code}
-module plta.Modules where
+module plfa.Modules where
 \end{code}
 
 This chapter introduces modules as a way of structuring proofs,

src/plfa/plta/More.lagda

@@ -5,7 +5,7 @@ permalink : /More/
 ---
 
 \begin{code}
-module plta.More where
+module plfa.More where
 \end{code}
 
 So far, we have focussed on a relatively minimal language,

src/plfa/plta/Naturals.lagda

@@ -5,7 +5,7 @@ permalink : /Naturals/
 ---
 
 \begin{code}
-module plta.Naturals where
+module plfa.Naturals where
 \end{code}
 
 The night sky holds more stars than I can count, though fewer than five

src/plfa/plta/Negation.lagda

@@ -5,7 +5,7 @@ permalink : /Negation/
 ---
 
 \begin{code}
-module plta.Negation where
+module plfa.Negation where
 \end{code}
 
 This chapter introduces negation, and discusses intuitionistic

src/plfa/plta/Preface.lagda

@@ -4,10 +4,6 @@ layout    : page
 permalink : /Preface/
 ---
 
-\begin{code}
-module plta.Preface where
-\end{code}
-
 The most profound connection between logic and computation is a pun.
 The doctrine of Propositions as Types asserts that a certain kind of formal
 structure may be read in two ways: either as a proposition in logic or

src/plfa/plta/Properties.lagda

@@ -5,7 +5,7 @@ permalink : /Properties/
 ---
 
 \begin{code}
-module plta.Properties where
+module plfa.Properties where
 \end{code}
 
 [Parts of this chapter take their text from chapter _StlcProp_

src/plfa/plta/Quantifiers.lagda

@@ -5,7 +5,7 @@ permalink : /Quantifiers/
 ---
 
 \begin{code}
-module plta.Quantifiers where
+module plfa.Quantifiers where
 \end{code}
 
 This chapter introduces universal and existential quantification.

src/plfa/plta/Relations.lagda

@@ -5,7 +5,7 @@ permalink : /Relations/
 ---
 
 \begin{code}
-module plta.Relations where
+module plfa.Relations where
 \end{code}
 
 After having defined operations such as addition and multiplication,

src/plfa/plta/Statistics.lagda

@@ -4,10 +4,6 @@ layout    : page
 permalink : /Statistics/
 ---
 
-\begin{code}
-module plta.Statistics where
-\end{code}
-
 Total number of lines and number of lines of Agda code in each chapter
 (as of 2 July 2018).
 

src/plfa/plta/Untyped.lagda

@@ -5,7 +5,7 @@ permalink : /Untyped/
 ---
 
 \begin{code}
-module plta.Untyped where
+module plfa.Untyped where
 \end{code}
 
 This chapter considers a system that varies, in interesting ways,