Daniel R. Grayson

definitions

1

Here's an example where we use a judgmental equality incorrectly. What should we do instead?

Theorem 3.1.2

9

Lots of rephrasing needed here.

read chapter 3 and fix the usage of \eqto and \eq

subtypes

1

In 2.16 we introduce connected components and call them subtypes, but subtypes aren't introduced until 2.20. We also speak of two components being the "same", and we write an equation...

" merely "

2

There must be a better word than "merely" we can use. In ordinary English, "merely" means "only", and that doesn't work with our use of it. Consider : X and...

"merely"

5

After our discussion of \eq and \eqto, I think this make no sense at all: How can we have a English adjectival phrase encoded by a type that is not...

In this text: the predicate `isnType` is undefined. Also, it would look better if the `n` occurred as a subscript, instead of inline.

identity type usage

19

Here is an example where an identity type is used in a sentence as though it were a proposition: This is likely to cause confusion.

The validator complains if we don't specify a character encoding. A change like this might be good, for we can also tell emacs the character encoding to use: ``` diff...

Html tags inside rawhtml sections in *_bib.html files should be displayed in quoted form, or else the validator complains. E.g., change ``` abstract = { \begin{rawhtml} In this paper we...