Steve Awodey
Steve Awodey
How about adding it as a Remark or Exercise? Sent from my iPhone > On Nov 30, 2019, at 01:28, Mike Shulman wrote: > > Thanks for this suggestion. But...
but the best is an article _and_ a blog post announcing it and explaining the main ideas. : - ) Sent from my iPhone > On Oct 2, 2014, at...
Sent from my iPhone > On Mar 7, 2015, at 12:44 PM, Andrej Bauer [email protected] wrote: > > I have in the past used truth value where it was customary...
wait — I thought fractions were a joke. are you really serious about fractional theorem numbers? On Jan 15, 2014, at 6:21 PM, Mike Shulman [email protected] wrote: > Another thought:...
what, again, is the advantage over the more conventional decimal scheme?
the problem with 4.6.10.1 is that next time one doesn’t know whether to use 4.6.10.2 or 4.6.10.1.1 ? On Jan 15, 2014, at 11:40 PM, Mike Shulman [email protected] wrote: >...
4.6.10.01?
On Jan 16, 2014, at 10:05 AM, Andrej Bauer [email protected] wrote: > And also, this is way cool. > > the real reason ...
ah, good point — we are not the first people to face this problem, and librarians have probaby already solved it. On Jan 16, 2014, at 9:41 PM, Vladimir Voevodsky...
The correct form of elimination and computation rules for the higher constructors of HITs is a somewhat delicate matter - and still open to different approaches. See section 6.2 for...