backwards open-quotation marks in exercise 4 of worksheet 1

[annag42]

In problem 4 of the first Worksheet here [1] [2], there appear to be two instances of a close-quotation mark at the start of a phrase [3] [4], where an open-quotation mark would be more conventional than a close-quotation mark. Each instance was possibly generated from either '' (two single-tick marks) or " (a double-tick mark) in LaTeX source, and could be generated in the more-conventional direction (resulting, instead, in an open-quotation mark) by instead using `` (two back-tick marks).

[1] path: Worksheets/ws1.pdf
[2] permalink: https://github.com/martinescardo/HoTTEST-Summer-School/blob/834375d587b3a7d1103b1c044b25d593b461198d/Worksheets/ws1.pdf
[3] phrase: types are theorems
[4] phrase: programs are proofs

[Schippmunk]

Thanks for your contribution. The quotes have been addressed.