On January 12, 2020 10:17:49 AM PST, vvs <[email protected]> wrote:
>I have no opinion about Bourbaki, though. That might be the problem... 

Heh, maybe it is a generational thing because I look at the HoTT book as the 
thing to be studied and formalized.

Like Bourbaki, it was written by a number of collaborators (even I contributed 
a sentence via pull request). Like Bourbaki it aims to summarize and 
systematize mathematics.

Now, it covers far fewer topics than Bourbaki and I'm not even sure what I 
think about the premise of the book (type theory in general, or univalent 
dependent type theory in particular) or certain topics (e.g. surreal numbers).

But I guess I understand the nerdy impulse to read math books (or write 
metamath proofs) rather than, say, keep up with the latest TV series.

-- 
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/5222B993-C089-461B-9F9D-474B1664224A%40panix.com.

Reply via email to