martinescardo/hottest-summer-school

HoTTEST Summer School materials

hottest-summer-school's Issues

backwards open-quotation marks in exercise 4 of worksheet 1

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