I wanted to share the pdf I've written so far but it didn't send and I lost what I wrote. I guess attachments aren't allowed. I'll post a link instead.
pdf file <https://1drv.ms/b/s!AuvNPSOQfN3xjKxgB2QVuLZMOT_W5Q?e=FCRy2b> On Monday, July 3, 2023 at 11:31:45 PM UTC-4 [email protected] wrote: > On 7/3/23 15:56, Marshall Stoner wrote: > > > have written up everything I considered prior to the definition of the > > biconditional and conjugation. > > . . . will attach and share what I have written so far as soon as I > > know that I am approved for the mailing list. . . . > > I'll be curious to see what you came up with and how you organize it. We > have some ways of organizing material on the website, for example "How > to intuitionize classical proofs" at > https://us.metamath.org/ileuni/mmil.html#intuitionize , "Real and > Complex Numbers" at https://us.metamath.org/mpeuni/mmcomplex.html , or > "Algebraic and Topological Structures" at > https://us.metamath.org/mpeuni/mmtopstr.html . All of these link to > relevant theorems but add explanations or give some structure in terms > of how one statement relates to another. > > Making pull requests to the web site should now be possible but feel > free to ask if it isn't clear where files go, whether website scripts > need to be changed, etc. > > Semi-relatedly, someone recently asked on Mastodon what a good source > for the constructive ordinals is. There have been three suggestions so > far. One is a normal math book (the HoTT book). The other two are > collections of formalized proofs (iset.mm and TypeToplogy). And neither > of the latter two give you an especially good idea of where to find the > ordinal stuff and where to start. It got me thinking about how to make > the material we have easy to read especially in cases where noone has > written a textbook which lays everything out carefully with the purpose > of teaching. Anyway, the thread is > https://mathstodon.xyz/@boarders/110646213816213644 in case anyone is > interested. > > > -- 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/77ecbdd0-a0e5-4977-aa66-aa772768a651n%40googlegroups.com.
