Use https instead of http where possible

Notes.md

@@ -64,7 +64,7 @@ Get evidence!
 >      Manage Users and Edit
 > to the Google Analytics account `plfa (UA-125055580)` by `wen.kokke@gmail.com`.
 
-> [Google analytics](http://analytics.google.com/analytics/web/)
+> [Google analytics](https://analytics.google.com/analytics/web/)
 
 ## Where to put Lists?
 

README.md

@@ -129,7 +129,7 @@ Command to give when in a hole:
 	C-c C-.      Goal type, context, and inferred type
 
 See
-[the emacs-mode docs](http://agda.readthedocs.io/en/latest/tools/emacs-mode.html)
+[the emacs-mode docs](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html)
 for more details.
 
 If you want to see messages beside rather than below your Agda code,
@@ -175,4 +175,4 @@ The book is written in [Kramdown Markdown](https://kramdown.gettalong.org/syntax
 
 ## Travis Continuous Integration
 
-You can view the build history of PLFA at [travis-ci.org](http://travis-ci.org/plfa/plfa.github.io).
+You can view the build history of PLFA at [travis-ci.org](https://travis-ci.org/plfa/plfa.github.io).

index.md

@@ -56,6 +56,6 @@ Pull requests are encouraged.
     * John Leo, Google Seattle, 2018--2019
 
 [wen]: https://github.com/wenkokke
-[phil]: http://homepages.inf.ed.ac.uk/wadler/
+[phil]: https://homepages.inf.ed.ac.uk/wadler/
 [GitHub]: https://github.com/plfa/plfa.github.io/
-[sbmf]: http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
+[sbmf]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf

src/plfa/Preface.lagda

@@ -92,12 +92,12 @@ 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/
+[tapl]: https://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
+[ta]: https://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf
+[stump]: https://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908
 [wen]: https://github.com/wenkokke
-[phil]: http://homepages.inf.ed.ac.uk/wadler/
+[phil]: https://homepages.inf.ed.ac.uk/wadler/
 
 ## A word on the exercises
 

tspl/TSPL.lagda

@@ -7,7 +7,7 @@ permalink : /TSPL/
 ## Staff
 
 * **Instructor**
-    [Philip Wadler](http://homepages.inf.ed.ac.uk/wadler)
+    [Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
 * **Teaching assistants**
   - [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
   - [Chad Nester](mailto:chad.nester@gmail.com)