On Sunday, January 12, 2020 at 11:51:10 PM UTC+1, Jim Kingdon wrote: > > Heh, maybe it is a generational thing because I look at the HoTT book as > the thing to be studied and formalized. >
Please note that Bourbaki was not brought up in this discussion (in the link I gave above) as the thing to be studied and formalized, but merely because its TOC could serve as a guide for ordering the sections of set.mm. Benoît -- 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/0068ad45-3ac5-43bc-b82c-e1767602e31e%40googlegroups.com.
