>
> 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/82afee8e-1329-422a-955e-e4ab852996e1%40googlegroups.com.

Reply via email to