Steve Awodey
Steve Awodey
good thing somebody knows what’s where! On Feb 23, 2014, at 2:01 PM, Mike Shulman [email protected] wrote: > @awodey's second suggestion is Corollary 5.8.5, and @EgbertRijke's is almost the same...
Yes - very nice! I think Dan G has recently formalized this. Sent from my iPhone > On Apr 11, 2014, at 7:24 PM, Mike Shulman [email protected] wrote: > >...
I don’t think that the fact that a proof assistant requires something is a very good reason to do it *informally* : - ) isn’t it enough to have a...
> yes to Andrej's proposed statement about separating discussion of the Book from general discussion.
the problem with this is that it’s easier to say what it _is_ about than what it is _not_ about, since the scope of the latter will keep changing as...
OK with me. will you draft something? > On Feb 2, 2015, at 10:23 PM, Mike Shulman [email protected] wrote: > > Yes, it's a moving target, but I think since...
I agree. Sent from my iPhone > On Oct 17, 2014, at 5:16 PM, Andrej Bauer [email protected] wrote: > > I think the problem is that the Introduction is very...
of course, Benedikt and coauthors have recently written a paper on this that could be cited. Steve > On Apr 22, 2015, at 5:51 PM, Mike Shulman [email protected] wrote: >...
check. > On Apr 22, 2015, at 7:36 PM, Mike Shulman [email protected] wrote: > > (which Sophie linked to in her first comment) > > — > Reply to this...
I actually disagree and prefer to use the word “term” also for semantics, but I think I lost that argument and agreed to “point” as a compromise. “Element” is simply...