(This group is manually moderated, so posts may not appear immediately.) On Tue, Jul 4, 2023 at 2:04 AM Marshall Stoner <[email protected]> wrote:
> 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 > <https://groups.google.com/d/msgid/metamath/77ecbdd0-a0e5-4977-aa66-aa772768a651n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs%2BMUj%2BoSEKMOcFA4CgsTYTqjkWaU9t%2B4zEX6m51901DA%40mail.gmail.com.
