Steve Awodey
Steve Awodey
it was a comment by Martin Escardo. > On May 14, 2015, at 3:56 PM, Mike Shulman [email protected] wrote: > > I think we noticed this on the list a...
I’m not really involved in the book (yet), but I think this issue is worth an in-person discussion — especially after Dan’s talk today, which reminded us again of how...
another thing we'll need if it's going to go to libraries is a Library of Congress entry (look on the copyright page of any book and you will see the...
I doubt it -- why should they? And why would they be any more able to do it than us? They don't have a tech report series or similar --...
here's the LOC thing: http://www.loc.gov/publish/cip/ On Jun 21, 2013, at 6:11 PM, Mike Shulman [email protected] wrote: > Will the ISBN remain constant as we post updates to the book? Do...
can we crowd-source this, too? On Jun 21, 2013, at 6:18 PM, steve awodey [email protected] wrote: > here's the LOC thing: > > http://www.loc.gov/publish/cip/ > > On Jun 21, 2013,...
Yes. Sent from my iPhone On Jun 22, 2013, at 5:06 PM, Andrej Bauer [email protected] wrote: > You mean, is there someone listening who knows how to do this? >...
Show that the universe is not a "0-type” (in the terms to be introduced in Chapter 3): it is not the case that parallel paths are always equal. (Hint: use...
that’s OK — the reader is still in chapter 2! we can even add a reference from there back to the exercise. On Feb 21, 2014, at 7:58 PM, Mike...
How about something like this: Show that the univalence axiom (for a universe U) is equivalent to the following principle of “equivalence induction" for U: given any family of types...