> > Heh, maybe it is a generational thing because I look at the HoTT book as > the thing to be studied and formalized. >
HoTT is a small book compared to the one by Bourbaki. I don't know what's in it anymore (type or category theory) but in my opinion it will be as usual: it will not supplant the other points of view, but it will be added to the others. If you take a book by Knuth, you'll notice that his favorite style of math is 19th century math, and that's interesting. If you take the formalization of typed lambda calculus, you will soon notice that they quickly jump to formalized set theory in this new framework. And Benoît recalls in the post below that he just wants to use Bourbaki's treatise table of content. No more. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/82afee8e-1329-422a-955e-e4ab852996e1%40googlegroups.com.
