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.
- Re: [Metamath] Re: Please move metamath 100 results into... David A. Wheeler
- Re: [Metamath] Re: Please move metamath 100 results... savask
- Re: [Metamath] Re: Please move metamath 100 res... David A. Wheeler
- Re: [Metamath] Re: Please move metamath 100 res... 'fl' via Metamath
- Re: [Metamath] Re: Please move metamath 100... Benoit
- Re: [Metamath] Re: Please move metamath... 'fl' via Metamath
- Re: [Metamath] Re: Please move metamath 100... 'fl' via Metamath
- Re: [Metamath] Re: Please move metamath... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... vvs
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... Jim Kingdon
- Re: [Metamath] Re: Please move met... Benoit
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... vvs
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... 'fl' via Metamath
- Re: [Metamath] Re: Please move met... vvs
