Philip Wadler
Philip Wadler
Thank you for the feedback. It is helpful to understand what readers find difficult. However, your claim that subst is the first use of Set other than T : Set...
Thanks for pointing this out. I suggest you write out a full solution to the problem using one of the proposed techniques, and then submit a pull request to modify...
Waiting on CI to work before accepting a change to Agda code. I hope CI will be fixed soon!
Good point. Probably a better way forward is to change the problem to just show that M ~ N implies M † ≡ N.
@ywata I am impressed! Nice idea. Thank you. Yes, I like the proposal to repeat characters three times in Part I and twice in Part II. Am I right that...
Thank you. All good points! It's fairly subtle, so I'm not sure whether the best thing is to explain these points or delete the exercise. If someone suggests appropriate text,...
The section on extensionality in Chapter Isomorphism now states: "More generally, we may wish to postulate extensionality for dependent functions" and introduces a suitable postulate named ∀-extensionality. So all that...
I called it an embedding because one often refers to embedding/projection pairs, which is exactly what to and from form. The point that ⊥ ↪ ⊤ is inhabited, while ⊥...
Makes sense. (I would do it if "make test" was running, but since it isn't it seems a bit dangerous.)
Thanks, Matthew! Excellent point. I think the right way to fix this is to introduce proj_1 and proj_2 directly for existentials when they are introduced. As I recall, Wen wanted...